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

proof

let x be object ; :: 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 A1: x in dom ([:f,h:] * <:g,k:>) ; :: thesis: x in dom <:(f * g),(h * k):>
then A2: x in dom <:g,k:> by FUNCT_1:11;
then A3: x in (dom g) /\ (dom k) by Def7;
then A4: x in dom g by XBOOLE_0:def 4;
A5: x in dom k by A3, XBOOLE_0:def 4;
<:g,k:> . x in dom [:f,h:] by A1, FUNCT_1:11;
then [(g . x),(k . x)] in dom [:f,h:] by A2, Def7;
then A6: [(g . x),(k . x)] in [:(dom f),(dom h):] by Def8;
then k . x in dom h by ZFMISC_1:87;
then A7: x in dom (h * k) by A5, FUNCT_1:11;
g . x in dom f by A6, ZFMISC_1:87;
then x in dom (f * g) by A4, FUNCT_1:11;
then x in (dom (f * g)) /\ (dom (h * k)) by A7, XBOOLE_0:def 4;
hence x in dom <:(f * g),(h * k):> by Def7; :: thesis: verum

end;

assume x in dom <:(f * g),(h * k):> ; :: thesis: x in dom ([:f,h:] * <:g,k:>)
then A8: x in (dom (f * g)) /\ (dom (h * k)) by Def7;
then A9: x in dom (f * g) by XBOOLE_0:def 4;
A10: x in dom (h * k) by A8, XBOOLE_0:def 4;
then A11: x in dom k by FUNCT_1:11;
x in dom g by A9, FUNCT_1:11;
then x in (dom g) /\ (dom k) by A11, XBOOLE_0:def 4;
then A12: x in dom <:g,k:> by Def7;
A13: k . x in dom h by A10, FUNCT_1:11;
g . x in dom f by A9, FUNCT_1:11;
then [(g . x),(k . x)] in [:(dom f),(dom h):] by A13, ZFMISC_1:87;
then [(g . x),(k . x)] in dom [:f,h:] by Def8;
then <:g,k:> . x in dom [:f,h:] by A12, Def7;
hence x in dom ([:f,h:] * <:g,k:>) by A12, FUNCT_1:11; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in dom ([:f,h:] * <:g,k:>) implies ([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x )
assume A15: x in dom ([:f,h:] * <:g,k:>) ; :: thesis: ([:f,h:] * <:g,k:>) . x = <:(f * g),(h * k):> . x
then A16: x in dom <:g,k:> by FUNCT_1:11;
then A17: x in (dom g) /\ (dom k) by Def7;
then A18: x in dom g by XBOOLE_0:def 4;
<:g,k:> . x in dom [:f,h:] by A15, FUNCT_1:11;
then [(g . x),(k . x)] in dom [:f,h:] by A16, Def7;
then A19: [(g . x),(k . x)] in [:(dom f),(dom h):] by Def8;
then A20: g . x in dom f by ZFMISC_1:87;
A21: x in dom k by A17, XBOOLE_0:def 4;
A22: k . x in dom h by A19, ZFMISC_1:87;
then A23: x in dom (h * k) by A21, FUNCT_1:11;
x in dom (f * g) by A20, A18, FUNCT_1:11;
then A24: x in (dom (f * g)) /\ (dom (h * k)) by A23, XBOOLE_0:def 4;
thus ([:f,h:] * <:g,k:>) . x = [:f,h:] . (<:g,k:> . x) by A15, FUNCT_1:12
.= [:f,h:] . ((g . x),(k . x)) by A16, Def7
.= [(f . (g . x)),(h . (k . x))] by A20, A22, Def8
.= [((f * g) . x),(h . (k . x))] by A18, FUNCT_1:13
.= [((f * g) . x),((h * k) . x)] by A21, FUNCT_1:13
.= <:(f * g),(h * k):> . x by A24, Th48 ; :: thesis: verum

end;

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