let f1, f2 be Function of (Union the Sorts of (Free (S,X))),(bool (X . s)); :: thesis: ( ( for t being Element of (Free (S,X)) holds f1 . t = (S variables_in t) . s ) & ( for t being Element of (Free (S,X)) holds f2 . t = (S variables_in t) . s ) implies f1 = f2 )
assume that
A1: for t being Element of (Free (S,X)) holds f1 . t = (S variables_in t) . s and
A2: for t being Element of (Free (S,X)) holds f2 . t = (S variables_in t) . s ; :: thesis: f1 = f2

now :: thesis: for x being Element of Union the Sorts of (Free (S,X)) holds f1 . x = f2 . x

let x be Element of Union the Sorts of (Free (S,X)); :: thesis: f1 . x = f2 . x
reconsider t = x as Element of (Free (S,X)) ;
thus f1 . x = (S variables_in t) . s by A1
.= f2 . x by A2 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum