let I be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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)); :: thesis: 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; :: thesis: ( g = y . n implies g . i in the Sorts of (A . i) . s )
assume g = y . n ; :: thesis: 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; :: thesis: verum