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