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

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:113; :: thesis: verum