defpred S1[ set ] means ( P2[$1] & $1 in F3() );
defpred S2[ set ] means ( P1[$1] & $1 in F3() );
deffunc H1( set ) -> set = F5() . $1;
deffunc H2( set ) -> set = F4() . $1;
set C = { H1(v') where v' is Element of F1() : S2[v'] } ;
A3:
for v being Element of F1() holds
( S2[v] iff S1[v] )
by A2;
A4:
{ H1(v') where v' is Element of F1() : S2[v'] } = { H1(v') where v' is Element of F1() : S1[v'] }
from FRAENKEL:sch 3(A3);
A5:
for v being Element of F1() st S2[v] holds
H2(v) = H1(v)
by A1, Th3;
{ H2(u') where u' is Element of F1() : S2[u'] } = { H1(v') where v' is Element of F1() : S2[v'] }
from FRAENKEL:sch 6(A5);
hence
{ (F4() . u') where u' is Element of F1() : ( P1[u'] & u' in F3() ) } = { (F5() . v') where v' is Element of F1() : ( P2[v'] & v' in F3() ) }
by A4; :: thesis: verum