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

end;

assume q in [:(f " B),(g " A):] ; :: thesis: q in [:f,g:] " [:B,A:]
then consider x1, x2 being set such that
A5: x1 in f " B and
A6: x2 in g " A and
A7: q = [x1,x2] by ZFMISC_1:def 2;
( x1 in dom f & x2 in dom g & f . x1 in B & g . x2 in A ) by A5, A6, FUNCT_1:def 13;
then ( [x1,x2] in [:(dom f),(dom g):] & [:(dom f),(dom g):] = dom [:f,g:] & [:f,g:] . x1,x2 = [(f . x1),(g . x2)] & [(f . x1),(g . x2)] in [:B,A:] ) by Def9, ZFMISC_1:106;
hence q in [:f,g:] " [:B,A:] by A7, FUNCT_1:def 13; :: thesis: verum

end;

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