let f, g, h, k be Function; :: thesis: [:f,h:] * [:g,k:] = [:(f * g),(h * k):]
A1: for x, y being object st x in dom (f * g) & y in dom (h * k) holds
([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y)

proof

let x, y be object ; :: thesis: ( x in dom (f * g) & y in dom (h * k) implies ([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y) )
assume that
A2: x in dom (f * g) and
A3: y in dom (h * k) ; :: thesis: ([:f,h:] * [:g,k:]) . (x,y) = [:(f * g),(h * k):] . (x,y)
A4: ( g . x in dom f & k . y in dom h ) by A2, A3, FUNCT_1:11;
A5: ( x in dom g & y in dom k ) by A2, A3, FUNCT_1:11;
then [x,y] in [:(dom g),(dom k):] by ZFMISC_1:87;
then [x,y] in dom [:g,k:] by Def8;
hence ([:f,h:] * [:g,k:]) . (x,y) = [:f,h:] . ([:g,k:] . (x,y)) by FUNCT_1:13
.= [:f,h:] . ((g . x),(k . y)) by A5, Def8
.= [(f . (g . x)),(h . (k . y))] by A4, Def8
.= [((f * g) . x),(h . (k . y))] by A2, FUNCT_1:12
.= [((f * g) . x),((h * k) . y)] by A3, FUNCT_1:12
.= [:(f * g),(h * k):] . (x,y) by A2, A3, Def8 ;
:: thesis: verum

end;

for p being object holds
( p in dom ([:f,h:] * [:g,k:]) iff p in [:(dom (f * g)),(dom (h * k)):] )

proof

let p be object ; :: thesis: ( p in dom ([:f,h:] * [:g,k:]) iff p in [:(dom (f * g)),(dom (h * k)):] )
A6: dom [:g,k:] = [:(dom g),(dom k):] by Def8;
A7: dom [:f,h:] = [:(dom f),(dom h):] by Def8;
thus ( p in dom ([:f,h:] * [:g,k:]) implies p in [:(dom (f * g)),(dom (h * k)):] ) :: thesis: ( p in [:(dom (f * g)),(dom (h * k)):] implies p in dom ([:f,h:] * [:g,k:]) )

proof

assume A8: p in dom ([:f,h:] * [:g,k:]) ; :: thesis: p in [:(dom (f * g)),(dom (h * k)):]
then A9: [:g,k:] . p in dom [:f,h:] by FUNCT_1:11;
A10: p in dom [:g,k:] by A8, FUNCT_1:11;
then consider x1, x2 being object such that
A11: x1 in dom g and
A12: x2 in dom k and
A13: p = [x1,x2] by A6, ZFMISC_1:def 2;
[:g,k:] . (x1,x2) = [:g,k:] . p by A13;
then A14: [(g . x1),(k . x2)] in dom [:f,h:] by A6, A10, A9, A13, Th65;
then k . x2 in dom h by A7, ZFMISC_1:87;
then A15: x2 in dom (h * k) by A12, FUNCT_1:11;
g . x1 in dom f by A7, A14, ZFMISC_1:87;
then x1 in dom (f * g) by A11, FUNCT_1:11;
hence p in [:(dom (f * g)),(dom (h * k)):] by A13, A15, ZFMISC_1:87; :: thesis: verum

end;

assume p in [:(dom (f * g)),(dom (h * k)):] ; :: thesis: p in dom ([:f,h:] * [:g,k:])
then consider x1, x2 being object such that
A16: ( x1 in dom (f * g) & x2 in dom (h * k) ) and
A17: p = [x1,x2] by ZFMISC_1:def 2;
( x1 in dom g & x2 in dom k ) by A16, FUNCT_1:11;
then A18: [x1,x2] in dom [:g,k:] by A6, ZFMISC_1:87;
( g . x1 in dom f & k . x2 in dom h ) by A16, FUNCT_1:11;
then [(g . x1),(k . x2)] in dom [:f,h:] by A7, ZFMISC_1:87;
then [:g,k:] . (x1,x2) in dom [:f,h:] by A6, A18, Th65;
hence p in dom ([:f,h:] * [:g,k:]) by A17, A18, FUNCT_1:11; :: thesis: verum

end;

then A19: dom ([:f,h:] * [:g,k:]) = [:(dom (f * g)),(dom (h * k)):] by TARSKI:2;
[:(dom (f * g)),(dom (h * k)):] = dom [:(f * g),(h * k):] by Def8;
hence [:f,h:] * [:g,k:] = [:(f * g),(h * k):] by A19, A1, Th6; :: thesis: verum