let S be non empty non void ManySortedSign ; :: thesis: for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds

for f being ManySortedFunction of A1,A2

for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let A1, A2, B1, B2 be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) implies for f being ManySortedFunction of A1,A2

for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y )

assume A1: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) ) ; :: thesis: for f being ManySortedFunction of A1,A2

for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let f be ManySortedFunction of A1,A2; :: thesis: for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let g be ManySortedFunction of B1,B2; :: thesis: ( f = g implies for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y )

assume A2: f = g ; :: thesis: for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let o be OperSymbol of S; :: thesis: ( Args (o,A1) <> {} & Args (o,A2) <> {} implies for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y )

assume A3: ( Args (o,A1) <> {} & Args (o,A2) <> {} ) ; :: thesis: for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let x be Element of Args (o,A1); :: thesis: for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let y be Element of Args (o,B1); :: thesis: ( x = y implies f # x = g # y )

assume A4: x = y ; :: thesis: f # x = g # y

f # x = (Frege (f * (the_arity_of o))) . x by A3, MSUALG_3:def 5;

hence f # x = g # y by A1, A2, A3, A4, MSUALG_3:def 5; :: thesis: verum

for f being ManySortedFunction of A1,A2

for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let A1, A2, B1, B2 be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) implies for f being ManySortedFunction of A1,A2

for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y )

assume A1: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) ) ; :: thesis: for f being ManySortedFunction of A1,A2

for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let f be ManySortedFunction of A1,A2; :: thesis: for g being ManySortedFunction of B1,B2 st f = g holds

for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let g be ManySortedFunction of B1,B2; :: thesis: ( f = g implies for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y )

assume A2: f = g ; :: thesis: for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds

for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let o be OperSymbol of S; :: thesis: ( Args (o,A1) <> {} & Args (o,A2) <> {} implies for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y )

assume A3: ( Args (o,A1) <> {} & Args (o,A2) <> {} ) ; :: thesis: for x being Element of Args (o,A1)

for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let x be Element of Args (o,A1); :: thesis: for y being Element of Args (o,B1) st x = y holds

f # x = g # y

let y be Element of Args (o,B1); :: thesis: ( x = y implies f # x = g # y )

assume A4: x = y ; :: thesis: f # x = g # y

f # x = (Frege (f * (the_arity_of o))) . x by A3, MSUALG_3:def 5;

hence f # x = g # y by A1, A2, A3, A4, MSUALG_3:def 5; :: thesis: verum