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 () 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 ;
reconsider pi1 = () /. n2, pi2 = () /. n2 as Element of S1 ;
A7: (the_arity_of o1) /. n2 = () . n2 by ;
A8: the_arity_of o1 <= the_arity_of o2 by A2;
then len () = len () ;
then dom () = dom () by FINSEQ_3:29;
then (the_arity_of o2) /. n2 = () . n2 by ;
then A9: pi1 <= pi2 by A4, A6, A8, A7;
rng () c= the carrier of S1 ;
then rng () c= dom the Sorts of U1 by PARTFUN1:def 2;
then A10: n2 in dom ( the Sorts of U1 * ()) by ;
dom (F . pi1) = the Sorts of U1 . pi1 by FUNCT_2:def 1
.= the Sorts of U1 . (() . n2) by
.= ( the Sorts of U1 * ()) . n2 by ;
then A11: x1 . n2 in dom (F . pi1) by ;
(F # x) . n2 = (F . (() /. n2)) . (x1 . n2) by
.= (F . pi2) . (x1 . n2) by A1, A11, A9
.= (F # x1) . n2 by ;
hence (F # x) . n1 = (F # x1) . n1 ; :: thesis: verum
end;
dom x1 = dom () by MSUALG_3:6;
then A12: dom (F # x1) = dom x1 by MSUALG_3:6;
dom (F # x) = dom x by ;
hence F # x = F # x1 by ; :: thesis: verum