let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S
for A being MSAlgebra over S
for C being MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let U0 be non-empty MSAlgebra over S; :: thesis: for A being MSAlgebra over S
for C being MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let A be MSAlgebra over S; :: thesis: for C being MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let C be MSSubAlgebra of A; :: thesis: for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let D be ManySortedSubset of the Sorts of A; :: thesis: ( D = the Sorts of C implies for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y )
assume A1: D = the Sorts of C ; :: thesis: for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let h be ManySortedFunction of A,U0; :: thesis: for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let g be ManySortedFunction of C,U0; :: thesis: ( g = h || D implies for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y )
assume A2: g = h || D ; :: thesis: for o being OperSymbol of S
for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let o be OperSymbol of S; :: thesis: for x being Element of Args (o,A)
for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let x be Element of Args (o,A); :: thesis: for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let y be Element of Args (o,C); :: thesis: ( Args (o,C) <> {} & x = y implies h # x = g # y )
assume that
A3: Args (o,C) <> {} and
A4: x = y ; :: thesis: h # x = g # y
set hx = h # x;
set gy = g # y;
set ar = the_arity_of o;
A5: y in Args (o,A) by A3, Th18;
then reconsider xx = x, yy = y as Function by MSUALG_6:1;
A6: dom yy = dom (the_arity_of o) by A3, MSUALG_3:6;
A7: dom xx = dom (the_arity_of o) by A5, MSUALG_3:6;

A8: now :: thesis: for n being object st n in dom (the_arity_of o) holds
(h # x) . n = (g # y) . n

let n be object ; :: thesis: ( n in dom (the_arity_of o) implies (h # x) . n = (g # y) . n )
assume A9: n in dom (the_arity_of o) ; :: thesis: (h # x) . n = (g # y) . n
then reconsider n9 = n as Nat ;
reconsider hn = h . ((the_arity_of o) . n) as Function of ( the Sorts of A . ((the_arity_of o) . n)),( the Sorts of U0 . ((the_arity_of o) . n)) by A9, PARTFUN1:4, PBOOLE:def 15;
(the_arity_of o) . n in the carrier of S by A9, PARTFUN1:4;
then A10: g . ((the_arity_of o) . n9) = hn | (D . ((the_arity_of o) . n)) by A2, MSAFREE:def 1;
dom ( the Sorts of C * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
then xx . n in ( the Sorts of C * (the_arity_of o)) . n by A3, A4, A9, MSUALG_3:6;
then A11: xx . n in D . ((the_arity_of o) . n) by A1, A9, FUNCT_1:13;
thus (h # x) . n = (h # x) . n9
.= (h . ((the_arity_of o) /. n)) . (xx . n) by A5, A7, A9, MSUALG_3:24
.= (h . ((the_arity_of o) . n)) . (xx . n) by A9, PARTFUN1:def 6
.= (g . ((the_arity_of o) . n)) . (xx . n) by A10, A11, FUNCT_1:49
.= (g . ((the_arity_of o) /. n)) . (yy . n) by A4, A9, PARTFUN1:def 6
.= (g # y) . n9 by A3, A6, A9, MSUALG_3:24
.= (g # y) . n ; :: thesis: verum

end;

( dom (h # x) = dom (the_arity_of o) & dom (g # y) = dom (the_arity_of o) ) by MSUALG_3:6;
hence h # x = g # y by A8, FUNCT_1:2; :: thesis: verum