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

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

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

dom x1 = dom (the_arity_of o2)
by MSUALG_3:6;
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;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

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