let X, Y, Z be set ; :: thesis: for f, g being Function st (rng f) /\ (dom g) c= Y holds
<:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>
let f, g be Function; :: thesis: ( (rng f) /\ (dom g) c= Y implies <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> )
assume A1: (rng f) /\ (dom g) c= Y ; :: thesis: <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>
A2: dom <:(g * f),X,Z:> c= dom (<:g,Y,Z:> * <:f,X,Y:>)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom <:(g * f),X,Z:> or x in dom (<:g,Y,Z:> * <:f,X,Y:>) )
assume A3: x in dom <:(g * f),X,Z:> ; :: thesis: x in dom (<:g,Y,Z:> * <:f,X,Y:>)
then A4: x in dom (g * f) by Th24;
then A5: f . x in dom g by FUNCT_1:11;
A6: x in dom f by A4, FUNCT_1:11;
then f . x in rng f by FUNCT_1:def 3;
then A7: f . x in (rng f) /\ (dom g) by A5, XBOOLE_0:def 4;
(g * f) . x in Z by A3, Th24;
then g . (f . x) in Z by A4, FUNCT_1:12;
then A8: f . x in dom <:g,Y,Z:> by A1, A5, A7, Th24;
( x in dom <:f,X,Y:> & <:f,X,Y:> . x = f . x ) by A1, A3, A6, A7, Th24, Th25;
hence x in dom (<:g,Y,Z:> * <:f,X,Y:>) by A8, FUNCT_1:11; :: thesis: verum

end;

for x being object st x in dom <:(g * f),X,Z:> holds
<:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x

proof

let x be object ; :: thesis: ( x in dom <:(g * f),X,Z:> implies <:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x )
assume A9: x in dom <:(g * f),X,Z:> ; :: thesis: <:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x
then A10: x in dom (g * f) by Th24;
then A11: f . x in dom g by FUNCT_1:11;
x in dom f by A10, FUNCT_1:11;
then f . x in rng f by FUNCT_1:def 3;
then A12: f . x in (rng f) /\ (dom g) by A11, XBOOLE_0:def 4;
(g * f) . x in Z by A9, Th24;
then g . (f . x) in Z by A10, FUNCT_1:12;
then A13: f . x in dom <:g,Y,Z:> by A1, A11, A12, Th24;
x in dom f by A10, FUNCT_1:11;
then A14: x in dom <:f,X,Y:> by A1, A9, A12, Th24;
thus <:(g * f),X,Z:> . x = (g * f) . x by A9, Th26
.= g . (f . x) by A10, FUNCT_1:12
.= <:g,Y,Z:> . (f . x) by A13, Th26
.= <:g,Y,Z:> . (<:f,X,Y:> . x) by A14, Th26
.= (<:g,Y,Z:> * <:f,X,Y:>) . x by A2, A9, FUNCT_1:12 ; :: thesis: verum

end;

then A15: <:(g * f),X,Z:> c= <:g,Y,Z:> * <:f,X,Y:> by A2, GRFUNC_1:2;
<:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:> by Th35;
hence <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> by A15; :: thesis: verum