set d = the Element of D;
reconsider F = the carrier' of C --> (id the Element of D) as Function of the carrier' of C, the carrier' of D ;
take F ; :: thesis: ( ( for c being Element of C ex d being Element of D st F . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f) ) )
thus for c being Element of C ex d being Element of D st F . (id c) = id d by FUNCOP_1:7; :: thesis: ( ( for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f) ) )
A1: Hom ( the Element of D, the Element of D) <> {} ;
thus for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) :: thesis: for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f)
proof
let f be Element of the carrier' of C; :: thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )
A2: F . f = id the Element of D by FUNCOP_1:7;
thus F . (id (dom f)) = id the Element of D by FUNCOP_1:7
.= id (dom (F . f)) by A2 ; :: thesis: F . (id (cod f)) = id (cod (F . f))
thus F . (id (cod f)) = id the Element of D by FUNCOP_1:7
.= id (cod (F . f)) by A2 ; :: thesis: verum
end;
let f, g be Element of the carrier' of C; :: thesis: ( [g,f] in dom the Comp of C implies F . (g (*) f) = (F . g) (*) (F . f) )
assume [g,f] in dom the Comp of C ; :: thesis: F . (g (*) f) = (F . g) (*) (F . f)
thus F . (g (*) f) = (id the Element of D) * (id the Element of D) by FUNCOP_1:7
.= (id the Element of D) (*) (id the Element of D) by A1, Def11
.= (id the Element of D) (*) (F . f) by FUNCOP_1:7
.= (F . g) (*) (F . f) by FUNCOP_1:7 ; :: thesis: verum