deffunc H₁( set ) -> Element of the carrier' of C = opp (F /. $1);
set A = the carrier' of C;
thus ( ex F being Function of I, the carrier' of C 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 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