set SS = AllSymbolsOf S;
let IT1, IT2 be Function of ((((AllSymbolsOf S) *) \ {{}}) *),(((AllSymbolsOf S) *) \ {{}}); :: thesis: ( ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds IT1 . V = s -compound V ) & ( for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds IT2 . V = s -compound V ) implies IT1 = IT2 )
assume that
B1: for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds IT1 . V = s -compound V and
B2: for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds IT2 . V = s -compound V ; :: thesis: IT1 = IT2

now

let V be Element of (((AllSymbolsOf S) *) \ {{}}) * ; :: thesis: IT1 . V = IT2 . V
thus IT1 . V = s -compound V by B1
.= IT2 . V by B2 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:def 7; :: thesis: verum