set A = { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ;
set B = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } ;
set C = { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ;
A3: { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } from FRAENKEL:sch 4(A1);
 { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } from LFUZZY_0:sch 3(A2);
 hence { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } by A3; :: thesis: verum