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 object ; :: 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 object such that
A2: z = [x,y] by RELAT_1:def 1;
y in union B by A1, A2, ZFMISC_1:87;
then consider b9 being set such that
A3: y in b9 and
A4: b9 in B by TARSKI:def 4;
x in union A by A1, A2, ZFMISC_1:87;
then consider a9 being set such that
A5: x in a9 and
A6: a9 in A by TARSKI:def 4;
reconsider b9 = b9 as Element of B by A4;
reconsider a9 = a9 as Element of A by A6;
A7: [:a9,b9:] in { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } ;
z in [:a9,b9:] 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 object ; :: 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 a9 being Element of A, b9 being Element of B such that
A10: [:a9,b9:] = e and
a9 in A and
b9 in B by A9;
consider x, y being object such that
A11: ( x in a9 & y in b9 ) 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