let X, Y, Z be set ; :: thesis: for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>
let f, g be Function; :: thesis: <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>
A1: for x being object st x in dom (<:g,Y,Z:> * <:f,X,Y:>) holds
(<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x

proof

let x be object ; :: thesis: ( x in dom (<:g,Y,Z:> * <:f,X,Y:>) implies (<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x )
assume A2: x in dom (<:g,Y,Z:> * <:f,X,Y:>) ; :: thesis: (<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x
then A3: x in dom <:f,X,Y:> by FUNCT_1:11;
then A4: x in dom f by Th24;
<:f,X,Y:> . x in dom <:g,Y,Z:> by A2, FUNCT_1:11;
then A5: f . x in dom <:g,Y,Z:> by A3, Th26;
then g . (f . x) in Z by Th24;
then A6: (g * f) . x in Z by A4, FUNCT_1:13;
f . x in dom g by A5, Th24;
then x in dom (g * f) by A4, FUNCT_1:11;
then A7: x in dom <:(g * f),X,Z:> by A2, A6, Th24;
thus (<:g,Y,Z:> * <:f,X,Y:>) . x = <:g,Y,Z:> . (<:f,X,Y:> . x) by A2, FUNCT_1:12
.= <:g,Y,Z:> . (f . x) by A3, Th26
.= g . (f . x) by A5, Th26
.= (g * f) . x by A4, FUNCT_1:13
.= <:(g * f),X,Z:> . x by A7, Th26 ; :: thesis: verum

end;

dom (<:g,Y,Z:> * <:f,X,Y:>) c= dom <:(g * f),X,Z:>

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (<:g,Y,Z:> * <:f,X,Y:>) or x in dom <:(g * f),X,Z:> )
assume A8: x in dom (<:g,Y,Z:> * <:f,X,Y:>) ; :: thesis: x in dom <:(g * f),X,Z:>
then A9: x in dom <:f,X,Y:> by FUNCT_1:11;
then A10: x in dom f by Th24;
<:f,X,Y:> . x in dom <:g,Y,Z:> by A8, FUNCT_1:11;
then A11: f . x in dom <:g,Y,Z:> by A9, Th26;
then g . (f . x) in Z by Th24;
then A12: (g * f) . x in Z by A10, FUNCT_1:13;
f . x in dom g by A11, Th24;
then x in dom (g * f) by A10, FUNCT_1:11;
hence x in dom <:(g * f),X,Z:> by A8, A12, Th24; :: thesis: verum

end;

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