let B, A be set ; :: thesis: for f, g being Function holds [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):]
let f, g be Function; :: thesis: [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):]
for q being set holds
( q in [:f,g:] .: [:B,A:] iff q in [:(f .: B),(g .: A):] )

proof

let q be set ; :: thesis: ( q in [:f,g:] .: [:B,A:] iff q in [:(f .: B),(g .: A):] )
thus ( q in [:f,g:] .: [:B,A:] implies q in [:(f .: B),(g .: A):] ) :: thesis: ( q in [:(f .: B),(g .: A):] implies q in [:f,g:] .: [:B,A:] )

proof

assume q in [:f,g:] .: [:B,A:] ; :: thesis: q in [:(f .: B),(g .: A):]
then consider p being set such that
A1: p in dom [:f,g:] and
A2: p in [:B,A:] and
A3: q = [:f,g:] . p by FUNCT_1:def 12;
dom [:f,g:] = [:(dom f),(dom g):] by Def9;
then consider x, y being set such that
A4: ( x in dom f & y in dom g ) and
A5: p = [x,y] by A1, ZFMISC_1:def 2;
A6: q = [:f,g:] . x,y by A3, A5;
( x in B & y in A ) by A2, A5, ZFMISC_1:106;
then ( f . x in f .: B & g . y in g .: A & q = [(f . x),(g . y)] ) by A4, A6, Def9, FUNCT_1:def 12;
hence q in [:(f .: B),(g .: A):] by ZFMISC_1:106; :: thesis: verum

end;

assume q in [:(f .: B),(g .: A):] ; :: thesis: q in [:f,g:] .: [:B,A:]
then consider y1, y2 being set such that
A7: y1 in f .: B and
A8: y2 in g .: A and
A9: q = [y1,y2] by ZFMISC_1:def 2;
consider x1 being set such that
A10: ( x1 in dom f & x1 in B ) and
A11: y1 = f . x1 by A7, FUNCT_1:def 12;
consider x2 being set such that
A12: ( x2 in dom g & x2 in A ) and
A13: y2 = g . x2 by A8, FUNCT_1:def 12;
( [x1,x2] in [:(dom f),(dom g):] & [:(dom f),(dom g):] = dom [:f,g:] & [x1,x2] in [:B,A:] & [:f,g:] . x1,x2 = [(f . x1),(g . x2)] ) by A10, A12, Def9, ZFMISC_1:106;
hence q in [:f,g:] .: [:B,A:] by A9, A11, A13, FUNCT_1:def 12; :: thesis: verum

end;

hence [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):] by TARSKI:2; :: thesis: verum