let C be semi-functional para-functional category; :: thesis: for a being object of st id (the_carrier_of a) in <^a,a^> holds
idm a = id (the_carrier_of a)
let a be object of ; :: thesis: ( id (the_carrier_of a) in <^a,a^> implies idm a = id (the_carrier_of a) )
assume id (the_carrier_of a) in <^a,a^> ; :: thesis: idm a = id (the_carrier_of a)
then reconsider f = id (the_carrier_of a) as Morphism of , ;

now

let b be object of ; :: thesis: ( <^a,b^> <> {} implies for g being Morphism of , holds g * f = g )
assume A1: <^a,b^> <> {} ; :: thesis: for g being Morphism of , holds g * f = g
let g be Morphism of ,; :: thesis: g * f = g
A2: dom g = the_carrier_of a by A1, Th36;
thus g * f = g * (id (the_carrier_of a)) by A1, Th38
.= g by A2, RELAT_1:78 ; :: thesis: verum

end;

hence idm a = id (the_carrier_of a) by ALTCAT_1:def 19; :: thesis: verum