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 A1: 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
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
let g be Function; :: thesis: ( g = y . n implies g . i in the Sorts of (A . i) . s )
assume A3: g = y . n ; :: thesis: g . i in the Sorts of (A . i) . s
A4: n in dom (the Sorts of (product A) * (the_arity_of o)) by A1, PRALG_2:10;
i in I ;
then A5: i in dom (Carrier A,s) by PARTFUN1:def 4;
y in Args o,(product A) ;
then y in product (the Sorts of (product A) * (the_arity_of o)) by PRALG_2:10;
then g in (the Sorts of (product A) * (the_arity_of o)) . n by A3, A4, CARD_3:18;
then g in the Sorts of (product A) . s by A2, A4, FUNCT_1:22;
then A6: g in product (Carrier A,s) by PRALG_2:def 17;
consider U0 being MSAlgebra of S such that
A7: ( U0 = A . i & (Carrier A,s) . i = the Sorts of U0 . s ) by PRALG_2:def 16;
thus g . i in the Sorts of (A . i) . s by A5, A6, A7, CARD_3:18; :: thesis: verum