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

proof

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

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

suppose F₃(s,F₂()) = TRUE ; :: thesis: (Fid (g1,F₁())) . s = (Fid (g2,F₁())) . s

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

end;

suppose A9: F₃(s,F₂()) <> TRUE ; :: thesis: (Fid (g1,F₁())) . s = (Fid (g2,F₁())) . s

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

end;

end;

end;

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