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;
x in union A by A1, A2, ZFMISC_1:106;
then consider a' being set such that
A3: ( x in a' & a' in A ) by TARSKI:def 4;
y in union B by A1, A2, ZFMISC_1:106;
then consider b' being set such that
A4: ( y in b' & b' in B ) by TARSKI:def 4;
reconsider a' = a' as Element of A by A3;
reconsider b' = b' as Element of B by A4;
A5: z in [:a',b':] by A2, A3, A4, ZFMISC_1:def 2;
[:a',b':] in { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } ;
hence z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } by A5, 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
A6: ( z in e & 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
A7: ( [:a',b':] = e & a' in A & b' in B ) by A6;
consider x, y being set such that
A8: ( x in a' & y in b' & z = [x,y] ) by A6, A7, ZFMISC_1:def 2;
( x in union A & y in union B ) by A8, TARSKI:def 4;
hence z in [:(union A),(union B):] by A8, ZFMISC_1:def 2; :: thesis: verum