let f, g, h, k be Function; :: thesis: [:f,h:] * <:g,k:> = <:(f * g),(h * k):>
for x being set holds
( x in dom ([:f,h:] * <:g,k:>) iff x in dom <:(f * g),(h * k):> )

proof

let x be set ; :: thesis: ( x in dom ([:f,h:] * <:g,k:>) iff x in dom <:(f * g),(h * k):> )
thus ( x in dom ([:f,h:] * <:g,k:>) implies x in dom <:(f * g),(h * k):> ) :: thesis: ( x in dom <:(f * g),(h * k):> implies x in dom ([:f,h:] * <:g,k:>) )

proof

assume x in dom ([:f,h:] * <:g,k:>) ; :: thesis: x in dom <:(f * g),(h * k):>
then ( x in dom <:g,k:> & <:g,k:> . x in dom [:f,h:] ) by FUNCT_1:21;
then ( x in dom <:g,k:> & [(g . x),(k . x)] in dom [:f,h:] ) by Def8;
then ( [(g . x),(k . x)] in [:(dom f),(dom h):] & x in (dom g) /\ (dom k) ) by Def8, Def9;
then ( g . x in dom f & k . x in dom h & x in dom g & x in dom k ) by XBOOLE_0:def 4, ZFMISC_1:106;
then ( x in dom (f * g) & x in dom (h * k) ) by FUNCT_1:21;
then x in (dom (f * g)) /\ (dom (h * k)) by XBOOLE_0:def 4;
hence x in dom <:(f * g),(h * k):> by Def8; :: thesis: verum

end;

assume x in dom <:(f * g),(h * k):> ; :: thesis: x in dom ([:f,h:] * <:g,k:>)
then x in (dom (f * g)) /\ (dom (h * k)) by Def8;
then ( x in dom (f * g) & x in dom (h * k) ) by XBOOLE_0:def 4;
then ( g . x in dom f & k . x in dom h & x in dom g & x in dom k ) by FUNCT_1:21;
then ( [(g . x),(k . x)] in [:(dom f),(dom h):] & x in (dom g) /\ (dom k) ) by XBOOLE_0:def 4, ZFMISC_1:106;
then ( [(g . x),(k . x)] in dom [:f,h:] & x in dom <:g,k:> ) by Def8, Def9;
then ( <:g,k:> . x in dom [:f,h:] & x in dom <:g,k:> ) by Def8;
hence x in dom ([:f,h:] * <:g,k:>) by FUNCT_1:21; :: thesis: verum

end;

then A1: dom ([:f,h:] * <:g,k:>) = dom <:(f * g),(h * k):> by TARSKI:2;
for x being set st x in dom ([:f,h:] * <:g,k:>) holds
([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x

proof

let x be set ; :: thesis: ( x in dom ([:f,h:] * <:g,k:>) implies ([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x )
assume A2: x in dom ([:f,h:] * <:g,k:>) ; :: thesis: ([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x
then A3: ( x in dom <:g,k:> & <:g,k:> . x in dom [:f,h:] ) by FUNCT_1:21;
then [(g . x),(k . x)] in dom [:f,h:] by Def8;
then ( [(g . x),(k . x)] in [:(dom f),(dom h):] & x in (dom g) /\ (dom k) ) by A3, Def8, Def9;
then A4: ( g . x in dom f & k . x in dom h & x in dom g & x in dom k ) by XBOOLE_0:def 4, ZFMISC_1:106;
then ( x in dom (f * g) & x in dom (h * k) ) by FUNCT_1:21;
then A5: x in (dom (f * g)) /\ (dom (h * k)) by XBOOLE_0:def 4;
thus ([:f,h:] * <:g,k:>) . x = [:f,h:] . (<:g,k:> . x) by A2, FUNCT_1:22
.= [:f,h:] . (g . x),(k . x) by A3, Def8
.= [(f . (g . x)),(h . (k . x))] by A4, Def9
.= [((f * g) . x),(h . (k . x))] by A4, FUNCT_1:23
.= [((f * g) . x),((h * k) . x)] by A4, FUNCT_1:23
.= <:(f * g),(h * k):> . x by A5, Th68 ; :: thesis: verum

end;

hence [:f,h:] * <:g,k:> = <:(f * g),(h * k):> by A1, FUNCT_1:9; :: thesis: verum