let S be non empty non void ManySortedSign ; 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; 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; 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; 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; for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)
let x be Element of Args (o,U1); (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
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 ;
( 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)
;
((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
;
verum
end;
( dom ((H2 ** H1) # x) = dom (the_arity_of o) & dom (H2 # (H1 # x)) = dom (the_arity_of o) )
by Th6;
hence
(H2 ** H1) # x = H2 # (H1 # x)
by A3, FUNCT_1:2; verum