deffunc H_{1}( set ) -> Element of the carrier' of (C opp) = (F /. $1) opp ;

set A = the carrier' of (C opp);

thus ( ex F being Function of I, the carrier' of (C opp) st

for x being set st x in I holds

F /. x = H_{1}(x) & ( for F1, F2 being Function of I, the carrier' of (C opp) st ( for x being set st x in I holds

F1 /. x = H_{1}(x) ) & ( for x being set st x in I holds

F2 /. x = H_{1}(x) ) holds

F1 = F2 ) ) from CAT_3:sch 2(); :: thesis: verum

set A = the carrier' of (C opp);

thus ( ex F being Function of I, the carrier' of (C opp) st

for x being set st x in I holds

F /. x = H

F1 /. x = H

F2 /. x = H

F1 = F2 ) ) from CAT_3:sch 2(); :: thesis: verum