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

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

hence
f1 = f2
; :: thesis: verum
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;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