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 A6: ( ( for o being OperSymbol of S holds f1 . o = o /. A ) & ( for o being OperSymbol of S holds f2 . o = o /. A ) ) ; :: thesis: f1 = f2
for x being set st x in the carrier' of S holds
f1 . x = f2 . x

proof

let x be set ; :: 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 & f2 . o1 = o1 /. A ) by A6;
hence f1 . x = f2 . x ; :: thesis: verum

end;

hence f1 = f2 by PBOOLE:3; :: thesis: verum