let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for i being Element of NAT st i in dom (the_arity_of o) holds
for A1, A2 being MSAlgebra over S
for h being ManySortedFunction of A1,A2
for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
let o be OperSymbol of S; :: thesis: for i being Element of NAT st i in dom (the_arity_of o) holds
for A1, A2 being MSAlgebra over S
for h being ManySortedFunction of A1,A2
for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
let i be Element of NAT ; :: thesis: ( i in dom (the_arity_of o) implies for A1, A2 being MSAlgebra over S
for h being ManySortedFunction of A1,A2
for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) )
assume A1: i in dom (the_arity_of o) ; :: thesis: for A1, A2 being MSAlgebra over S
for h being ManySortedFunction of A1,A2
for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
let A1, A2 be MSAlgebra over S; :: thesis: for h being ManySortedFunction of A1,A2
for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
let h be ManySortedFunction of A1,A2; :: thesis: for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds
for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
let a, b be Element of Args (o,A1); :: thesis: ( a in Args (o,A1) & h # a in Args (o,A2) implies for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) )
assume that
A2: a in Args (o,A1) and
A3: h # a in Args (o,A2) ; :: thesis: for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds
for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
reconsider f2 = b as Function by A2, Th1;
A4: dom f2 = dom (the_arity_of o) by A2, Th2;
let f, g1, g2 be Function; :: thesis: ( f = a & g1 = h # a & g2 = h # b implies for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) )
assume that
A5: f = a and
A6: g1 = h # a and
A7: g2 = h # b ; :: thesis: for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds
( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
reconsider g3 = g1 +* (i,(g2 . i)) as Function ;
A8: dom f = dom (the_arity_of o) by A2, A5, Th2;
let x be Element of A1,((the_arity_of o) /. i); :: thesis: ( b = f +* (i,x) implies ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) )
assume A9: b = f +* (i,x) ; :: thesis: ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) )
f2 . i = x by A1, A9, A8, FUNCT_7:31;
hence g2 . i = (h . ((the_arity_of o) /. i)) . x by A1, A2, A3, A7, A4, MSUALG_3:24; :: thesis: h # b = g1 +* (i,(g2 . i))
then g2 . i in the Sorts of A2 . ((the_arity_of o) /. i) by A1, A2, A3, Th8;
then g1 +* (i,(g2 . i)) in Args (o,A2) by A3, A6, Th7;
then A10: dom g3 = dom (the_arity_of o) by Th2;

A11: now :: thesis: for z being set st z in dom (the_arity_of o) & z <> i holds
g2 . z = g1 . z

let z be set ; :: thesis: ( z in dom (the_arity_of o) & z <> i implies g2 . z = g1 . z )
assume that
A12: z in dom (the_arity_of o) and
A13: z <> i ; :: thesis: g2 . z = g1 . z
reconsider j = z as Element of NAT by A12;
A14: f2 . j = f . j by A9, A13, FUNCT_7:32;
g2 . j = (h . ((the_arity_of o) /. j)) . (f2 . j) by A2, A3, A7, A4, A12, MSUALG_3:24;
hence g2 . z = g1 . z by A2, A3, A5, A6, A8, A12, A14, MSUALG_3:24; :: thesis: verum

end;

A15: dom g1 = dom (the_arity_of o) by A3, A6, Th2;

A16: now :: thesis: for z being object st z in dom (the_arity_of o) holds
g2 . z = (g1 +* (i,(g2 . i))) . z

let z be object ; :: thesis: ( z in dom (the_arity_of o) implies g2 . b₁ = (g1 +* (i,(g2 . i))) . b₁ )
assume A17: z in dom (the_arity_of o) ; :: thesis: g2 . b₁ = (g1 +* (i,(g2 . i))) . b₁

per cases ( z = i or z <> i ) ;

suppose z = i ; :: thesis: g2 . b₁ = (g1 +* (i,(g2 . i))) . b₁

hence g2 . z = (g1 +* (i,(g2 . i))) . z by A1, A15, FUNCT_7:31; :: thesis: verum

end;

suppose A18: z <> i ; :: thesis: g2 . b₁ = (g1 +* (i,(g2 . i))) . b₁

then g2 . z = g1 . z by A11, A17;
hence g2 . z = (g1 +* (i,(g2 . i))) . z by A18, FUNCT_7:32; :: thesis: verum

end;

end;

end;

dom g2 = dom (the_arity_of o) by A3, A7, Th2;
hence h # b = g1 +* (i,(g2 . i)) by A7, A10, A16, FUNCT_1:2; :: thesis: verum