let A, B 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 object holds
( q in [:f,g:] .: [:B,A:] iff q in [:(f .: B),(g .: A):] )

proof

let q be object ; :: thesis: ( q in [:f,g:] .: [:B,A:] iff q in [:(f .: B),(g .: A):] )
A1: [:(dom f),(dom g):] = dom [:f,g:] by Def8;
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 object such that
A2: p in dom [:f,g:] and
A3: p in [:B,A:] and
A4: q = [:f,g:] . p by FUNCT_1:def 6;
dom [:f,g:] = [:(dom f),(dom g):] by Def8;
then consider x, y being object such that
A5: x in dom f and
A6: y in dom g and
A7: p = [x,y] by A2, ZFMISC_1:def 2;
x in B by A3, A7, ZFMISC_1:87;
then A8: f . x in f .: B by A5, FUNCT_1:def 6;
y in A by A3, A7, ZFMISC_1:87;
then A9: g . y in g .: A by A6, FUNCT_1:def 6;
q = [:f,g:] . (x,y) by A4, A7;
then q = [(f . x),(g . y)] by A5, A6, Def8;
hence q in [:(f .: B),(g .: A):] by A8, A9, ZFMISC_1:87; :: thesis: verum

end;

assume q in [:(f .: B),(g .: A):] ; :: thesis: q in [:f,g:] .: [:B,A:]
then consider y1, y2 being object such that
A10: y1 in f .: B and
A11: y2 in g .: A and
A12: q = [y1,y2] by ZFMISC_1:def 2;
consider x1 being object such that
A13: x1 in dom f and
A14: x1 in B and
A15: y1 = f . x1 by A10, FUNCT_1:def 6;
consider x2 being object such that
A16: x2 in dom g and
A17: x2 in A and
A18: y2 = g . x2 by A11, FUNCT_1:def 6;
A19: [:f,g:] . (x1,x2) = [(f . x1),(g . x2)] by A13, A16, Def8;
( [x1,x2] in [:(dom f),(dom g):] & [x1,x2] in [:B,A:] ) by A13, A14, A16, A17, ZFMISC_1:87;
hence q in [:f,g:] .: [:B,A:] by A12, A15, A18, A1, A19, FUNCT_1:def 6; :: thesis: verum

end;

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