let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra over S
for s being SortSymbol of S
for a being Element of A,s
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s*> holds
for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*>
let A, B be non-empty MSAlgebra over S; :: thesis: for s being SortSymbol of S
for a being Element of A,s
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s*> holds
for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*>
let s be SortSymbol of S; :: thesis: for a being Element of A,s
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s*> holds
for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*>
let a be Element of A,s; :: thesis: for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s*> holds
for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*>
let h be ManySortedFunction of A,B; :: thesis: for o being OperSymbol of S st the_arity_of o = <*s*> holds
for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*>
let o be OperSymbol of S; :: thesis: ( the_arity_of o = <*s*> implies for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*> )
assume A1: the_arity_of o = <*s*> ; :: thesis: for p being Element of Args (o,A) st p = <*a*> holds
h # p = <*((h . s) . a)*>
let p be Element of Args (o,A); :: thesis: ( p = <*a*> implies h # p = <*((h . s) . a)*> )
assume A2: p = <*a*> ; :: thesis: h # p = <*((h . s) . a)*>
A3: ( dom p = dom (the_arity_of o) & dom (h # p) = dom (the_arity_of o) ) by MSUALG_3:6;
then A4: dom (h # p) = Seg 1 by A2, FINSEQ_1:38;
then A5: ( len p = 1 & len (h # p) = 1 ) by A3, FINSEQ_1:def 3;
1 in Seg 1 ;
then (h # p) . 1 = (h . ((the_arity_of o) /. 1)) . (p . 1) by A3, A4, MSUALG_3:def 6
.= (h . s) . (p . 1) by A1, FINSEQ_4:16
.= (h . s) . a by A2, FINSEQ_1:40 ;
hence h # p = <*((h . s) . a)*> by A5, FINSEQ_1:40; :: thesis: verum