let S1 be OrderSortedSign; for U1, U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted holds
for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let U1, U2 be non-empty OSAlgebra of S1; for F being ManySortedFunction of U1,U2 st F is order-sorted holds
for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let F be ManySortedFunction of U1,U2; ( F is order-sorted implies for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1 )
assume A1:
F is order-sorted
; for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let o1, o2 be OperSymbol of S1; ( o1 <= o2 implies for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1 )
assume A2:
o1 <= o2
; for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let x be Element of Args (o1,U1); for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let x1 be Element of Args (o2,U1); ( x = x1 implies F # x = F # x1 )
assume A3:
x = x1
; F # x = F # x1
A4:
dom x = dom (the_arity_of o1)
by MSUALG_3:6;
A5:
for n being object st n in dom x holds
(F # x) . n = (F # x1) . n
proof
let n1 be
object ;
( n1 in dom x implies (F # x) . n1 = (F # x1) . n1 )
assume A6:
n1 in dom x
;
(F # x) . n1 = (F # x1) . n1
reconsider n2 =
n1 as
Nat by A6, ORDINAL1:def 12;
reconsider pi1 =
(the_arity_of o1) /. n2,
pi2 =
(the_arity_of o2) /. n2 as
Element of
S1 ;
A7:
(the_arity_of o1) /. n2 = (the_arity_of o1) . n2
by A4, A6, PARTFUN1:def 6;
A8:
the_arity_of o1 <= the_arity_of o2
by A2;
then
len (the_arity_of o1) = len (the_arity_of o2)
;
then
dom (the_arity_of o1) = dom (the_arity_of o2)
by FINSEQ_3:29;
then
(the_arity_of o2) /. n2 = (the_arity_of o2) . n2
by A4, A6, PARTFUN1:def 6;
then A9:
pi1 <= pi2
by A4, A6, A8, A7;
rng (the_arity_of o1) c= the
carrier of
S1
;
then
rng (the_arity_of o1) c= dom the
Sorts of
U1
by PARTFUN1:def 2;
then A10:
n2 in dom ( the Sorts of U1 * (the_arity_of o1))
by A4, A6, RELAT_1:27;
dom (F . pi1) =
the
Sorts of
U1 . pi1
by FUNCT_2:def 1
.=
the
Sorts of
U1 . ((the_arity_of o1) . n2)
by A4, A6, PARTFUN1:def 6
.=
( the Sorts of U1 * (the_arity_of o1)) . n2
by A4, A6, FUNCT_1:13
;
then A11:
x1 . n2 in dom (F . pi1)
by A3, A10, MSUALG_3:6;
(F # x) . n2 =
(F . ((the_arity_of o1) /. n2)) . (x1 . n2)
by A3, A6, MSUALG_3:def 6
.=
(F . pi2) . (x1 . n2)
by A1, A11, A9
.=
(F # x1) . n2
by A3, A6, MSUALG_3:def 6
;
hence
(F # x) . n1 = (F # x1) . n1
;
verum
end;
dom x1 = dom (the_arity_of o2)
by MSUALG_3:6;
then A12:
dom (F # x1) = dom x1
by MSUALG_3:6;
dom (F # x) = dom x
by A4, MSUALG_3:6;
hence
F # x = F # x1
by A3, A12, A5, FUNCT_1:2; verum