set A = { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ;
set C = { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ;
for a being object holds
( a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } iff a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } )
proof
let a be object ; :: thesis: ( a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } iff a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } )
hereby :: thesis: ( a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } implies a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } )
assume a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ; :: thesis: a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] }
then consider u being Element of F1(), v being Element of F2() such that
A2: a = F3(u,v) and
A3: P1[u,v] ;
a = F4(u,v) by A1, A2, A3;
hence a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } by A3; :: thesis: verum
end;
assume a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ; :: thesis: a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] }
then consider u being Element of F1(), v being Element of F2() such that
A4: a = F4(u,v) and
A5: P1[u,v] ;
a = F3(u,v) by A1, A4, A5;
hence a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } by A5; :: thesis: verum
end;
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() : P1[u2,v2] } by TARSKI:2; :: thesis: verum