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(v9) where v9 is Element of F1() : S1[v9] } ;
A3:
for v being Element of F1() holds
( S1[v] iff S2[v] )
by A2;
A4:
{ H2(v9) where v9 is Element of F1() : S1[v9] } = { H2(v9) where v9 is Element of F1() : S2[v9] }
from FRAENKEL:sch 3(A3);
A5:
for v being Element of F1() st S1[v] holds
H1(v) = H2(v)
by A1, Th1;
{ H1(u9) where u9 is Element of F1() : S1[u9] } = { H2(v9) where v9 is Element of F1() : S1[v9] }
from FRAENKEL:sch 6(A5);
hence
{ (F4() . u9) where u9 is Element of F1() : ( P1[u9] & u9 in F3() ) } = { (F5() . v9) where v9 is Element of F1() : ( P2[v9] & v9 in F3() ) }
by A4; verum