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

proof

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

proof

assume x in dom <:(f * h),(g * h):> ; :: thesis: x in dom (<:f,g:> * h)
then A1: x in (dom (f * h)) /\ (dom (g * h)) by Def7;
then A2: x in dom (f * h) by XBOOLE_0:def 4;
x in dom (g * h) by A1, XBOOLE_0:def 4;
then A3: h . x in dom g by FUNCT_1:11;
h . x in dom f by A2, FUNCT_1:11;
then h . x in (dom f) /\ (dom g) by A3, XBOOLE_0:def 4;
then A4: h . x in dom <:f,g:> by Def7;
x in dom h by A2, FUNCT_1:11;
hence x in dom (<:f,g:> * h) by A4, FUNCT_1:11; :: thesis: verum

end;

assume A5: x in dom (<:f,g:> * h) ; :: thesis: x in dom <:(f * h),(g * h):>
then A6: x in dom h by FUNCT_1:11;
h . x in dom <:f,g:> by A5, FUNCT_1:11;
then A7: h . x in (dom f) /\ (dom g) by Def7;
then h . x in dom g by XBOOLE_0:def 4;
then A8: x in dom (g * h) by A6, FUNCT_1:11;
h . x in dom f by A7, XBOOLE_0:def 4;
then x in dom (f * h) by A6, FUNCT_1:11;
then x in (dom (f * h)) /\ (dom (g * h)) by A8, XBOOLE_0:def 4;
hence x in dom <:(f * h),(g * h):> by Def7; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in dom <:(f * h),(g * h):> implies <:(f * h),(g * h):> . x = (<:f,g:> * h) . x )
assume A10: x in dom <:(f * h),(g * h):> ; :: thesis: <:(f * h),(g * h):> . x = (<:f,g:> * h) . x
then A11: x in (dom (f * h)) /\ (dom (g * h)) by Def7;
then A12: x in dom (f * h) by XBOOLE_0:def 4;
then A13: x in dom h by FUNCT_1:11;
A14: x in dom (g * h) by A11, XBOOLE_0:def 4;
then A15: h . x in dom g by FUNCT_1:11;
h . x in dom f by A12, FUNCT_1:11;
then A16: h . x in (dom f) /\ (dom g) by A15, XBOOLE_0:def 4;
thus <:(f * h),(g * h):> . x = [((f * h) . x),((g * h) . x)] by A10, Def7
.= [(f . (h . x)),((g * h) . x)] by A12, FUNCT_1:12
.= [(f . (h . x)),(g . (h . x))] by A14, FUNCT_1:12
.= <:f,g:> . (h . x) by A16, Th48
.= (<:f,g:> * h) . x by A13, FUNCT_1:13 ; :: thesis: verum

end;

hence <:(f * h),(g * h):> = <:f,g:> * h by A9; :: thesis: verum