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