deffunc H1( object ) -> boolean object = F4($1,F2(),F3());
A1:
for s being object st s in F1() holds
H1(s) in BOOLEAN
by MARGREL1:def 12;
consider IT being Function of F1(),BOOLEAN such that
A2:
for s being object st s in F1() holds
IT . s = H1(s)
from FUNCT_2:sch 2(A1);
take
IT
; ( IT in ModelSP F1() & ( for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (IT,F1())) . s = TRUE ) ) )
IT in ModelSP F1()
by FUNCT_2:8;
then
Fid (IT,F1()) = IT
by Def41;
hence
( IT in ModelSP F1() & ( for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (IT,F1())) . s = TRUE ) ) )
by A2, FUNCT_2:8; verum