let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S

for U1, U2, U3 being non-empty MSAlgebra over S

for H1 being ManySortedFunction of U1,U2

for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let o be OperSymbol of S; :: thesis: for U1, U2, U3 being non-empty MSAlgebra over S

for H1 being ManySortedFunction of U1,U2

for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let U1, U2, U3 be non-empty MSAlgebra over S; :: thesis: for H1 being ManySortedFunction of U1,U2

for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let H1 be ManySortedFunction of U1,U2; :: thesis: for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let H2 be ManySortedFunction of U2,U3; :: thesis: for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let x be Element of Args (o,U1); :: thesis: (H2 ** H1) # x = H2 # (H1 # x)

A1: dom x = dom (the_arity_of o) by Th6;

A2: dom (H1 # x) = dom (the_arity_of o) by Th6;

A3: for y being object st y in dom (the_arity_of o) holds

((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y

hence (H2 ** H1) # x = H2 # (H1 # x) by A3, FUNCT_1:2; :: thesis: verum

for U1, U2, U3 being non-empty MSAlgebra over S

for H1 being ManySortedFunction of U1,U2

for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let o be OperSymbol of S; :: thesis: for U1, U2, U3 being non-empty MSAlgebra over S

for H1 being ManySortedFunction of U1,U2

for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let U1, U2, U3 be non-empty MSAlgebra over S; :: thesis: for H1 being ManySortedFunction of U1,U2

for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let H1 be ManySortedFunction of U1,U2; :: thesis: for H2 being ManySortedFunction of U2,U3

for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let H2 be ManySortedFunction of U2,U3; :: thesis: for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)

let x be Element of Args (o,U1); :: thesis: (H2 ** H1) # x = H2 # (H1 # x)

A1: dom x = dom (the_arity_of o) by Th6;

A2: dom (H1 # x) = dom (the_arity_of o) by Th6;

A3: for y being object st y in dom (the_arity_of o) holds

((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y

proof

( dom ((H2 ** H1) # x) = dom (the_arity_of o) & dom (H2 # (H1 # x)) = dom (the_arity_of o) )
by Th6;
rng (the_arity_of o) c= the carrier of S
by FINSEQ_1:def 4;

then rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def 2;

then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

let y be object ; :: thesis: ( y in dom (the_arity_of o) implies ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y )

assume A5: y in dom (the_arity_of o) ; :: thesis: ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y

then reconsider n = y as Nat ;

set F = H2 ** H1;

set p = (the_arity_of o) /. n;

A6: ((H2 ** H1) # x) . n = ((H2 ** H1) . ((the_arity_of o) /. n)) . (x . n) by A1, A5, Def6;

(the_arity_of o) /. n = (the_arity_of o) . n by A5, PARTFUN1:def 6;

then A7: ( the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) /. n) by A5, A4, FUNCT_1:12;

A8: (H2 ** H1) . ((the_arity_of o) /. n) = (H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n)) by Th2;

A9: dom (H1 . ((the_arity_of o) /. n)) = the Sorts of U1 . ((the_arity_of o) /. n) by FUNCT_2:def 1;

then dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))) = dom (H1 . ((the_arity_of o) /. n)) by FUNCT_2:def 1;

hence ((H2 ** H1) # x) . y = (H2 . ((the_arity_of o) /. n)) . ((H1 . ((the_arity_of o) /. n)) . (x . n)) by A5, A6, A4, A9, A7, A8, Th6, FUNCT_1:12

.= (H2 . ((the_arity_of o) /. n)) . ((H1 # x) . n) by A1, A5, Def6

.= (H2 # (H1 # x)) . y by A2, A5, Def6 ;

:: thesis: verum

end;then rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def 2;

then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

let y be object ; :: thesis: ( y in dom (the_arity_of o) implies ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y )

assume A5: y in dom (the_arity_of o) ; :: thesis: ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y

then reconsider n = y as Nat ;

set F = H2 ** H1;

set p = (the_arity_of o) /. n;

A6: ((H2 ** H1) # x) . n = ((H2 ** H1) . ((the_arity_of o) /. n)) . (x . n) by A1, A5, Def6;

(the_arity_of o) /. n = (the_arity_of o) . n by A5, PARTFUN1:def 6;

then A7: ( the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) /. n) by A5, A4, FUNCT_1:12;

A8: (H2 ** H1) . ((the_arity_of o) /. n) = (H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n)) by Th2;

A9: dom (H1 . ((the_arity_of o) /. n)) = the Sorts of U1 . ((the_arity_of o) /. n) by FUNCT_2:def 1;

then dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))) = dom (H1 . ((the_arity_of o) /. n)) by FUNCT_2:def 1;

hence ((H2 ** H1) # x) . y = (H2 . ((the_arity_of o) /. n)) . ((H1 . ((the_arity_of o) /. n)) . (x . n)) by A5, A6, A4, A9, A7, A8, Th6, FUNCT_1:12

.= (H2 . ((the_arity_of o) /. n)) . ((H1 # x) . n) by A1, A5, Def6

.= (H2 # (H1 # x)) . y by A2, A5, Def6 ;

:: thesis: verum

hence (H2 ** H1) # x = H2 # (H1 # x) by A3, FUNCT_1:2; :: thesis: verum