A3:
for u being Element of F1()
for v being Element of F2() st P2[u,v] holds
P1[u,v]
by A1;
A4:
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P2[u1,v1] } c= { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
from FRAENKEL:sch 2(A3);
deffunc H1( set , set ) -> set = F3($2,$1);
A5:
for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
P2[u,v]
by A1;
A6:
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } c= { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
from FRAENKEL:sch 2(A5);
A7:
for u being Element of F1()
for v being Element of F2() holds F3(u,v) = H1(u,v)
by A2;
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P2[u1,v1] } = { H1(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
from FRAENKEL:sch 7(A7);
hence
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F3(v2,u2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
by A6, A4, XBOOLE_0:def 10; verum