deffunc H₁( Element of the Sorts of (Free (S,X)) . s) -> Element of the Sorts of (Free (S,X)) . (the_sort_of C) = C -sub $1;
consider f being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) such that
A1: for t being Element of the Sorts of (Free (S,X)) . s holds f . t = H₁(t) from FUNCT_2:sch 4();
take f ; :: thesis: for t being Element of (Free (S,X)) st the_sort_of t = s holds
f . t = C -sub t
let t be Element of (Free (S,X)); :: thesis: ( the_sort_of t = s implies f . t = C -sub t )
assume the_sort_of t = s ; :: thesis: f . t = C -sub t
then t in the Sorts of (Free (S,X)) . s by SORT;
hence f . t = C -sub t by A1; :: thesis: verum