let C be semi-functional para-functional category; :: thesis: for a being Object of C st id (the_carrier_of a) in <^a,a^> holds
idm a = id (the_carrier_of a)
let a be Object of C; :: 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 a,a ;

now :: thesis: for b being Object of C st <^a,b^> <> {} holds
for g being Morphism of a,b holds g * f = g

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

end;

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