let S be non empty non void ManySortedSign ; 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; 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; 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; 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; 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; ( 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*>
; 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); ( p = <*a*> implies h # p = <*((h . s) . a)*> )
assume A2:
p = <*a*>
; 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; verum