let A, B be ManySortedFunction of ((ParsedTerms X) # ) * the Arity of S,(ParsedTerms X) * the ResultSort of S; :: thesis: ( ( for o being OperSymbol of S holds A . o = PTDenOp o,X ) & ( for o being OperSymbol of S holds B . o = PTDenOp o,X ) implies A = B )
assume that
A3: for o being OperSymbol of S holds A . o = PTDenOp o,X and
A4: for o being OperSymbol of S holds B . o = PTDenOp o,X ; :: thesis: A = B
for i being set st i in the carrier' of S holds
A . i = B . i

proof

let i be set ; :: thesis: ( i in the carrier' of S implies A . i = B . i )
assume i in the carrier' of S ; :: thesis: A . i = B . i
then reconsider s = i as OperSymbol of S ;
( A . s = PTDenOp s,X & B . s = PTDenOp s,X ) by A3, A4;
hence A . i = B . i ; :: thesis: verum

end;

hence A = B by PBOOLE:3; :: thesis: verum