let h1, h2 be set ; :: thesis: ( h1 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h1,F₁())) . s = TRUE ) ) & h2 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h2,F₁())) . s = TRUE ) ) implies h1 = h2 )
assume that
A1: h1 in ModelSP F₁() and
A2: for s being set st s in F₁() holds
( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h1,F₁())) . s = TRUE ) and
A3: h2 in ModelSP F₁() and
A4: for s being set st s in F₁() holds
( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h2,F₁())) . s = TRUE ) ; :: thesis: h1 = h2
A5: for s being set st s in F₁() holds
(Fid (h1,F₁())) . s = (Fid (h2,F₁())) . s

proof

let s be set ; :: thesis: ( s in F₁() implies (Fid (h1,F₁())) . s = (Fid (h2,F₁())) . s )
assume A6: s in F₁() ; :: thesis: (Fid (h1,F₁())) . s = (Fid (h2,F₁())) . s
set F1 = F₄(s,F₂(),F₃());
set f1 = (Fid (h1,F₁())) . s;
A7: ( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h1,F₁())) . s = TRUE ) by A2, A6;
set f2 = (Fid (h2,F₁())) . s;
A8: ( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h2,F₁())) . s = TRUE ) by A4, A6;

per cases ( F₄(s,F₂(),F₃()) = TRUE or F₄(s,F₂(),F₃()) <> TRUE ) ;

suppose F₄(s,F₂(),F₃()) = TRUE ; :: thesis: (Fid (h1,F₁())) . s = (Fid (h2,F₁())) . s

hence (Fid (h1,F₁())) . s = (Fid (h2,F₁())) . s by A4, A6, A7; :: thesis: verum

end;

suppose A9: F₄(s,F₂(),F₃()) <> TRUE ; :: thesis: (Fid (h1,F₁())) . s = (Fid (h2,F₁())) . s

then (Fid (h1,F₁())) . s = FALSE by A6, A7, Lm35;
hence (Fid (h1,F₁())) . s = (Fid (h2,F₁())) . s by A6, A8, A9, Lm35; :: thesis: verum

end;

end;

end;

h1 = Fid (h1,F₁()) by A1, Def43
.= Fid (h2,F₁()) by A5, FUNCT_2:12
.= h2 by A3, Def43 ;
hence h1 = h2 ; :: thesis: verum