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

for v being Element of F_{2}() st P_{2}[u,v] holds

P_{1}[u,v]
by A1;

A4: { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{2}[u1,v1] } c= { F_{3}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{1}[u2,v2] }
from FRAENKEL:sch 2(A3);

deffunc H_{1}( set , set ) -> object = F_{3}($2,$1);

A5: for u being Element of F_{1}()

for v being Element of F_{2}() st P_{1}[u,v] holds

P_{2}[u,v]
by A1;

A6: { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } c= { F_{3}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{2}[u2,v2] }
from FRAENKEL:sch 2(A5);

A7: for u being Element of F_{1}()

for v being Element of F_{2}() holds F_{3}(u,v) = H_{1}(u,v)
by A2;

{ F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{2}[u1,v1] } = { H_{1}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{2}[u2,v2] }
from FRAENKEL:sch 7(A7);

hence { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } = { F_{3}(v2,u2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{2}[u2,v2] }
by A6, A4; :: thesis: verum

for v being Element of F

P

A4: { F

deffunc H

A5: for u being Element of F

for v being Element of F

P

A6: { F

A7: for u being Element of F

for v being Element of F

{ F

hence { F