let A, B be non empty set ; :: thesis: [:(union A),(union B):] = union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
set Y = { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } ;
thus [:(union A),(union B):] c= union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } :: according to XBOOLE_0:def 10 :: thesis: union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } c= [:(union A),(union B):]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(union A),(union B):] or z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } )
assume A1: z in [:(union A),(union B):] ; :: thesis: z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
then consider x, y being set such that
A2: z = [x,y] by RELAT_1:def 1;
y in union B by A1, A2, ZFMISC_1:106;
then consider b' being set such that
A3: y in b' and
A4: b' in B by TARSKI:def 4;
x in union A by A1, A2, ZFMISC_1:106;
then consider a' being set such that
A5: x in a' and
A6: a' in A by TARSKI:def 4;
reconsider b' = b' as Element of B by A4;
reconsider a' = a' as Element of A by A6;
A7: [:a',b':] in { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } ;
z in [:a',b':] by A2, A5, A3, ZFMISC_1:def 2;
hence z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } by A7, TARSKI:def 4; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } or z in [:(union A),(union B):] )
assume z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } ; :: thesis: z in [:(union A),(union B):]
then consider e being set such that
A8: z in e and
A9: e in { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } by TARSKI:def 4;
consider a' being Element of A, b' being Element of B such that
A10: [:a',b':] = e and
a' in A and
b' in B by A9;
consider x, y being set such that
A11: ( x in a' & y in b' ) and
A12: z = [x,y] by A8, A10, ZFMISC_1:def 2;
( x in union A & y in union B ) by A11, TARSKI:def 4;
hence z in [:(union A),(union B):] by A12, ZFMISC_1:def 2; :: thesis: verum