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) & dom x1 = dom (the_arity_of o2) ) by MSUALG_3:6;
then A5: dom (F # x) = dom x by MSUALG_3:6;
A6: dom (F # x1) = dom x1 by A4, MSUALG_3:6;
for n being set st n in dom x holds
(F # x) . n = (F # x1) . n

proof

let n1 be set ; :: thesis: ( n1 in dom x implies (F # x) . n1 = (F # x1) . n1 )
assume A7: n1 in dom x ; :: thesis: (F # x) . n1 = (F # x1) . n1
reconsider n2 = n1 as Nat by A7, ORDINAL1:def 13;
reconsider pi1 = (the_arity_of o1) /. n2, pi2 = (the_arity_of o2) /. n2 as Element of S1 ;
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 4;
then A8: n2 in dom (the Sorts of U1 * (the_arity_of o1)) by A4, A7, RELAT_1:46;
dom (F . pi1) = the Sorts of U1 . pi1 by FUNCT_2:def 1
.= the Sorts of U1 . ((the_arity_of o1) . n2) by A4, A7, PARTFUN1:def 8
.= (the Sorts of U1 * (the_arity_of o1)) . n2 by A4, A7, FUNCT_1:23 ;
then A9: x1 . n2 in dom (F . pi1) by A3, A8, MSUALG_3:6;
A10: ( the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by A2, OSALG_1:def 22;
then len (the_arity_of o1) = len (the_arity_of o2) by OSALG_1:def 7;
then dom (the_arity_of o1) = dom (the_arity_of o2) by FINSEQ_3:31;
then ( (the_arity_of o1) /. n2 = (the_arity_of o1) . n2 & (the_arity_of o2) /. n2 = (the_arity_of o2) . n2 ) by A4, A7, PARTFUN1:def 8;
then A11: pi1 <= pi2 by A4, A7, A10, OSALG_1:def 7;
(F # x) . n2 = (F . ((the_arity_of o1) /. n2)) . (x1 . n2) by A3, A7, MSUALG_3:def 8
.= (F . pi2) . (x1 . n2) by A1, A9, A11, Def1
.= (F # x1) . n2 by A3, A7, MSUALG_3:def 8 ;
hence (F # x) . n1 = (F # x1) . n1 ; :: thesis: verum

end;

hence F # x = F # x1 by A3, A5, A6, FUNCT_1:9; :: thesis: verum