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 of 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 of 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 of 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 of 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 of 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:33;
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

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:34;
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

let z be set ; :: 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:33; :: 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:34; :: 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:9; :: thesis: verum