let I be non empty set ; for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let S be non empty non void ManySortedSign ; for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let A be MSAlgebra-Family of I,S; for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let o be OperSymbol of S; for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let i be Element of I; for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let n be set ; ( n in dom (the_arity_of o) implies for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s )
assume
n in dom (the_arity_of o)
; for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
then A1:
n in dom ( the Sorts of (product A) * (the_arity_of o))
by PRALG_2:3;
let s be SortSymbol of S; ( s = (the_arity_of o) . n implies for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s )
assume A2:
s = (the_arity_of o) . n
; for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
let y be Element of Args (o,(product A)); for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
y in Args (o,(product A))
;
then A3:
y in product ( the Sorts of (product A) * (the_arity_of o))
by PRALG_2:3;
let g be Function; ( g = y . n implies g . i in the Sorts of (A . i) . s )
assume
g = y . n
; g . i in the Sorts of (A . i) . s
then
g in ( the Sorts of (product A) * (the_arity_of o)) . n
by A1, A3, CARD_3:9;
then
g in the Sorts of (product A) . s
by A2, A1, FUNCT_1:12;
then A4:
g in product (Carrier (A,s))
by PRALG_2:def 10;
i in I
;
then A5:
i in dom (Carrier (A,s))
by PARTFUN1:def 2;
ex U0 being MSAlgebra over S st
( U0 = A . i & (Carrier (A,s)) . i = the Sorts of U0 . s )
by PRALG_2:def 9;
hence
g . i in the Sorts of (A . i) . s
by A5, A4, CARD_3:9; verum