let S be non empty non void ManySortedSign ; 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; 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; 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; 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; ( 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
; 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; 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; ( 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
; 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; 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); 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); ( Args (o,C) <> {} & x = y implies h # x = g # y )
assume that
A3:
Args (o,C) <> {}
and
A4:
x = y
; 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 for n being object st n in dom (the_arity_of o) holds
(h # x) . n = (g # y) . nlet n be
object ;
( n in dom (the_arity_of o) implies (h # x) . n = (g # y) . n )assume A9:
n in dom (the_arity_of o)
;
(h # x) . n = (g # y) . nthen 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
;
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; verum