let S1 be OrderSortedSign; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let x1 be Element of Args (o2,U1); :: thesis: ( x = x1 implies F # x = F # x1 )
assume A3: x = x1 ; :: thesis: 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 ; :: thesis: ( n1 in dom x implies (F # x) . n1 = (F # x1) . n1 )
assume A6: n1 in dom x ; :: thesis: (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 ; :: thesis: 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; :: thesis: verum