let f1, f2 be ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S; :: thesis: ( ( for o being OperSymbol of S holds f1 . o = o /. A ) & ( for o being OperSymbol of S holds f2 . o = o /. A ) implies f1 = f2 )
assume that
A3: for o being OperSymbol of S holds f1 . o = o /. A and
A4: for o being OperSymbol of S holds f2 . o = o /. A ; :: thesis: f1 = f2
for x being object st x in the carrier' of S holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in the carrier' of S implies f1 . x = f2 . x )
assume x in the carrier' of S ; :: thesis: f1 . x = f2 . x
then reconsider o1 = x as OperSymbol of S ;
f1 . o1 = o1 /. A by A3;
hence f1 . x = f2 . x by A4; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum