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

end;

assume q in [:(f " B),(g " A):] ; :: thesis: q in [:f,g:] " [:B,A:]
then consider x1, x2 being object such that
A8: ( x1 in f " B & x2 in g " A ) and
A9: q = [x1,x2] by ZFMISC_1:def 2;
( f . x1 in B & g . x2 in A ) by A8, FUNCT_1:def 7;
then A10: [(f . x1),(g . x2)] in [:B,A:] by ZFMISC_1:87;
( x1 in dom f & x2 in dom g ) by A8, FUNCT_1:def 7;
then A11: ( [x1,x2] in [:(dom f),(dom g):] & [:f,g:] . (x1,x2) = [(f . x1),(g . x2)] ) by Def8, ZFMISC_1:87;
[:(dom f),(dom g):] = dom [:f,g:] by Def8;
hence q in [:f,g:] " [:B,A:] by A9, A11, A10, FUNCT_1:def 7; :: thesis: verum

end;

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