deffunc H₁( 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₁(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₁(x) ) & ( for x being set st x in I holds
F2 /. x = H₁(x) ) holds
F1 = F2 ) ) from CAT_3:sch 2(); :: thesis: verum