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

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

hence
IT1 = IT2
by FUNCT_2:def 8; :: thesis: verumlet 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;thus IT1 . V = s -compound V by A2

.= IT2 . V by A3 ; :: thesis: verum