set A = { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } ;

set C = { F_{4}(u3,v3) where u3 is Element of F_{1}(), v3 is Element of F_{2}() : P_{1}[u3,v3] } ;

for a being object holds

( a in { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } iff a in { F_{4}(u3,v3) where u3 is Element of F_{1}(), v3 is Element of F_{2}() : P_{1}[u3,v3] } )
_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } = { F_{4}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{1}[u2,v2] }
by TARSKI:2; :: thesis: verum

set C = { F

for a being object holds

( a in { F

proof

hence
{ F
let a be object ; :: thesis: ( a in { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } iff a in { F_{4}(u3,v3) where u3 is Element of F_{1}(), v3 is Element of F_{2}() : P_{1}[u3,v3] } )

_{4}(u3,v3) where u3 is Element of F_{1}(), v3 is Element of F_{2}() : P_{1}[u3,v3] }
; :: thesis: a in { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] }

then consider u being Element of F_{1}(), v being Element of F_{2}() such that

A4: a = F_{4}(u,v)
and

A5: P_{1}[u,v]
;

a = F_{3}(u,v)
by A1, A4, A5;

hence a in { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] }
by A5; :: thesis: verum

end;hereby :: thesis: ( a in { F_{4}(u3,v3) where u3 is Element of F_{1}(), v3 is Element of F_{2}() : P_{1}[u3,v3] } implies a in { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } )

assume
a in { Fassume
a in { F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] }
; :: thesis: a in { F_{4}(u3,v3) where u3 is Element of F_{1}(), v3 is Element of F_{2}() : P_{1}[u3,v3] }

then consider u being Element of F_{1}(), v being Element of F_{2}() such that

A2: a = F_{3}(u,v)
and

A3: P_{1}[u,v]
;

a = F_{4}(u,v)
by A1, A2, A3;

hence a in { F_{4}(u3,v3) where u3 is Element of F_{1}(), v3 is Element of F_{2}() : P_{1}[u3,v3] }
by A3; :: thesis: verum

end;then consider u being Element of F

A2: a = F

A3: P

a = F

hence a in { F

then consider u being Element of F

A4: a = F

A5: P

a = F

hence a in { F