let f1, f2 be Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)); :: thesis: ( ( for t being Element of (Free (S,X)) st the_sort_of t = s holds
f1 . t = C -sub t ) & ( for t being Element of (Free (S,X)) st the_sort_of t = s holds
f2 . t = C -sub t ) implies f1 = f2 )
assume that
A1: for t being Element of (Free (S,X)) st the_sort_of t = s holds
f1 . t = C -sub t and
A2: for t being Element of (Free (S,X)) st the_sort_of t = s holds
f2 . t = C -sub t ; :: thesis: f1 = f2
let t be Element of the Sorts of (Free (S,X)) . s; :: according to PBOOLE:def 21 :: thesis: f1 . t = f2 . t
A3: the_sort_of t = s by SORT;
thus f1 . t = C -sub t by A1, A3
.= f2 . t by A2, A3 ; :: thesis: verum