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

proof

let x be set ; :: 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 x in (dom (f * h)) /\ (dom (g * h)) by Def8;
then A1: ( x in dom (f * h) & x in dom (g * h) ) by XBOOLE_0:def 4;
then ( h . x in dom f & h . x in dom g ) by FUNCT_1:21;
then h . x in (dom f) /\ (dom g) by XBOOLE_0:def 4;
then ( h . x in dom <:f,g:> & x in dom h ) by A1, Def8, FUNCT_1:21;
hence x in dom (<:f,g:> * h) by FUNCT_1:21; :: thesis: verum

end;

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

end;

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

proof

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

end;

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