deffunc H_{1}( set ) -> Element of the carrier of C = dom (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_{1}(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_{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;

thus ( ex F being Function of I, the carrier of C 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