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