let S be non empty non void ManySortedSign ; 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; 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; 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; 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; 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; 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; 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; ( 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*>
; 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); ( p = <*a,b,c*> implies h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*> )
assume A2:
p = <*a,b,c*>
; 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
;
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
;
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
;
hence
h # p = <*((h . s1) . a),((h . s2) . b),((h . s3) . c)*>
by A5, A6, A7, FINSEQ_1:45; verum