deffunc H_{1}( set ) -> set = F_{4}() . $1;

deffunc H_{2}( set ) -> set = F_{5}() . $1;

defpred S_{1}[ set ] means ( P_{1}[$1] & $1 in F_{3}() );

defpred S_{2}[ set ] means ( P_{2}[$1] & $1 in F_{3}() );

set C = { H_{2}(v9) where v9 is Element of F_{1}() : S_{1}[v9] } ;

A3: for v being Element of F_{1}() holds

( S_{1}[v] iff S_{2}[v] )
by A2;

A4: { H_{2}(v9) where v9 is Element of F_{1}() : S_{1}[v9] } = { H_{2}(v9) where v9 is Element of F_{1}() : S_{2}[v9] }
from FRAENKEL:sch 3(A3);

A5: for v being Element of F_{1}() st S_{1}[v] holds

H_{1}(v) = H_{2}(v)
by A1, Th1;

{ H_{1}(u9) where u9 is Element of F_{1}() : S_{1}[u9] } = { H_{2}(v9) where v9 is Element of F_{1}() : S_{1}[v9] }
from FRAENKEL:sch 6(A5);

hence { (F_{4}() . u9) where u9 is Element of F_{1}() : ( P_{1}[u9] & u9 in F_{3}() ) } = { (F_{5}() . v9) where v9 is Element of F_{1}() : ( P_{2}[v9] & v9 in F_{3}() ) }
by A4; :: thesis: verum

deffunc H

defpred S

defpred S

set C = { H

A3: for v being Element of F

( S

A4: { H

A5: for v being Element of F

H

{ H

hence { (F