let A, B be non empty set ; for C being set
for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds
g * f = id (dom f)
let C be set ; for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds
g * f = id (dom f)
let f, g be commuting Function; ( dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g implies g * f = id (dom f) )
assume that
A1:
dom f c= Funcs (A,(Funcs (B,C)))
and
A2:
rng f c= dom g
; g * f = id (dom f)
dom (g * f) = dom f
by A2, RELAT_1:27;
hence
g * f = id (dom f)
by A3, FUNCT_1:17; verum