let Y, Z, X 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: dom (<:g,Y,Z:> * <:f,X,Y:>) c= dom <:(g * f),X,Z:>

proof

let x be set ; :: 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 x in dom (<:g,Y,Z:> * <:f,X,Y:>) ; :: thesis: x in dom <:(g * f),X,Z:>
then ( x in dom <:f,X,Y:> & <:f,X,Y:> . x in dom <:g,Y,Z:> ) by FUNCT_1:21;
then ( x in dom f & x in X & f . x in dom <:g,Y,Z:> ) by Th78, Th80;
then ( x in dom f & x in X & f . x in dom g & g . (f . x) in Z ) by Th78;
then ( x in dom (g * f) & x in X & (g * f) . x in Z ) by FUNCT_1:21, FUNCT_1:23;
hence x in dom <:(g * f),X,Z:> by Th78; :: thesis: verum

end;

for x being set 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 set ; :: 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:> & <:f,X,Y:> . x in dom <:g,Y,Z:> ) by FUNCT_1:21;
then A4: ( x in dom f & x in X & f . x in dom <:g,Y,Z:> ) by Th78, Th80;
then ( x in dom f & x in X & f . x in dom g & g . (f . x) in Z ) by Th78;
then ( x in dom (g * f) & x in X & (g * f) . x in Z ) by FUNCT_1:21, FUNCT_1:23;
then A5: x in dom <:(g * f),X,Z:> by Th78;
thus (<:g,Y,Z:> * <:f,X,Y:>) . x = <:g,Y,Z:> . (<:f,X,Y:> . x) by A2, FUNCT_1:22
.= <:g,Y,Z:> . (f . x) by A3, Th80
.= g . (f . x) by A4, Th80
.= (g * f) . x by A4, FUNCT_1:23
.= <:(g * f),X,Z:> . x by A5, Th80 ; :: thesis: verum

end;

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