let h1, h2 be set ; :: thesis: ( h1 in ModelSP F1() & ( for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (h1,F1())) . s = TRUE ) ) & h2 in ModelSP F1() & ( for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (h2,F1())) . s = TRUE ) ) implies h1 = h2 )
assume that
A1: h1 in ModelSP F1() and
A2: for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (h1,F1())) . s = TRUE ) and
A3: h2 in ModelSP F1() and
A4: for s being set st s in F1() holds
( F4(s,F2(),F3()) = TRUE iff (Fid (h2,F1())) . s = TRUE ) ; :: thesis: h1 = h2
A5: for s being object st s in F1() holds
(Fid (h1,F1())) . s = (Fid (h2,F1())) . s
proof
let s be object ; :: thesis: ( s in F1() implies (Fid (h1,F1())) . s = (Fid (h2,F1())) . s )
assume A6: s in F1() ; :: thesis: (Fid (h1,F1())) . s = (Fid (h2,F1())) . s
set F1 = F4(s,F2(),F3());
set f1 = (Fid (h1,F1())) . s;
A7: ( F4(s,F2(),F3()) = TRUE iff (Fid (h1,F1())) . s = TRUE ) by A2, A6;
set f2 = (Fid (h2,F1())) . s;
A8: ( F4(s,F2(),F3()) = TRUE iff (Fid (h2,F1())) . s = TRUE ) by A4, A6;
per cases ( F4(s,F2(),F3()) = TRUE or F4(s,F2(),F3()) <> TRUE ) ;
suppose F4(s,F2(),F3()) = TRUE ; :: thesis: (Fid (h1,F1())) . s = (Fid (h2,F1())) . s
hence (Fid (h1,F1())) . s = (Fid (h2,F1())) . s by A4, A6, A7; :: thesis: verum
end;
suppose A9: F4(s,F2(),F3()) <> TRUE ; :: thesis: (Fid (h1,F1())) . s = (Fid (h2,F1())) . s
then (Fid (h1,F1())) . s = FALSE by A6, A7, Lm34;
hence (Fid (h1,F1())) . s = (Fid (h2,F1())) . s by A6, A8, A9, Lm34; :: thesis: verum
end;
end;
end;
h1 = Fid (h1,F1()) by A1, Def41
.= Fid (h2,F1()) by A5, FUNCT_2:12
.= h2 by A3, Def41 ;
hence h1 = h2 ; :: thesis: verum