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
A2: for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds IT1 . V = s -compound V and
A3: for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds IT2 . V = s -compound V ; :: thesis: IT1 = IT2
now :: thesis: for V being Element of (((AllSymbolsOf S) *) \ {{}}) * holds IT1 . V = IT2 . V
let V be Element of (((AllSymbolsOf S) *) \ {{}}) * ; :: thesis: IT1 . V = IT2 . V
thus IT1 . V = s -compound V by A2
.= IT2 . V by A3 ; :: thesis: verum
end;
hence IT1 = IT2 by FUNCT_2:def 8; :: thesis: verum