let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra over S
for s1, s2, s3 being SortSymbol of S
for a being Element of A,s1
for b being Element of A,s2
for c being Element of A,s3
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds
for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let A, B be non-empty MSAlgebra over S; :: thesis: for s1, s2, s3 being SortSymbol of S
for a being Element of A,s1
for b being Element of A,s2
for c being Element of A,s3
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds
for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let s1, s2, s3 be SortSymbol of S; :: thesis: for a being Element of A,s1
for b being Element of A,s2
for c being Element of A,s3
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds
for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let a be Element of A,s1; :: thesis: for b being Element of A,s2
for c being Element of A,s3
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds
for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let b be Element of A,s2; :: thesis: for c being Element of A,s3
for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds
for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let c be Element of A,s3; :: thesis: for h being ManySortedFunction of A,B
for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds
for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let h be ManySortedFunction of A,B; :: thesis: for o being OperSymbol of S st the_arity_of o = <*s1,s2,s3*> holds
for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let o be OperSymbol of S; :: thesis: ( the_arity_of o = <*s1,s2,s3*> implies for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*> )
assume A1: the_arity_of o = <*s1,s2,s3*> ; :: thesis: for p being Element of Args (o,A) st p = <*a,b,c*> holds
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
let p be Element of Args (o,A); :: thesis: ( p = <*a,b,c*> implies h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*> )
assume A2: p = <*a,b,c*> ; :: thesis: h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
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 3 by A2, FINSEQ_1:89;
then A5: ( len p = 3 & len (h # p) = 3 ) by A3, FINSEQ_1:def 3;
1 in Seg 3 ;
then A6: (h # p) . 1 = (h . ((the_arity_of o) /. 1)) . (p . 1) by A3, A4, MSUALG_3:def 6
.= (h . s1) . (p . 1) by A1, FINSEQ_4:18
.= (h . s1) . a by A2, FINSEQ_1:45 ;
2 in Seg 3 ;
then A7: (h # p) . 2 = (h . ((the_arity_of o) /. 2)) . (p . 2) by A3, A4, MSUALG_3:def 6
.= (h . s2) . (p . 2) by A1, FINSEQ_4:18
.= (h . s2) . b by A2, FINSEQ_1:45 ;
3 in Seg 3 ;
then (h # p) . 3 = (h . ((the_arity_of o) /. 3)) . (p . 3) by A3, A4, MSUALG_3:def 6
.= (h . s3) . (p . 3) by A1, FINSEQ_4:18
.= (h . s3) . c by A2, FINSEQ_1:45 ;
hence h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*> by A5, A6, A7, FINSEQ_1:45; :: thesis: verum