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