let f1, f2 be Function of S,S; :: thesis: ( ( for s being Element of S holds f1 . s = x "/\" s ) & ( for s being Element of S holds f2 . s = x "/\" s ) implies f1 = f2 )
assume that
A1: for s being Element of S holds f1 . s = x "/\" s and
A2: for s being Element of S holds f2 . s = x "/\" s ; :: thesis: f1 = f2

now :: thesis: for s being Element of S holds f1 . s = f2 . s

let s be Element of S; :: thesis: f1 . s = f2 . s
thus f1 . s = x "/\" s by A1
.= f2 . s by A2 ; :: thesis: verum

end;

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