let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2, U3 being non-empty MSAlgebra of 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 of 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 of 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 ((H2 ** H1) # x) = dom (the_arity_of o) & dom x = dom (the_arity_of o) & dom (H2 # (H1 # x)) = dom (the_arity_of o) & dom (H1 # x) = dom (the_arity_of o) )
by Th6;
for y being set st y in dom (the_arity_of o) holds
((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y
proof
let y be
set ;
:: thesis: ( y in dom (the_arity_of o) implies ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y )
assume A2:
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;
A3:
((H2 ** H1) # x) . n = ((H2 ** H1) . ((the_arity_of o) /. n)) . (x . n)
by A1, A2, Def8;
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 4;
then A4:
dom (the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:46;
A5:
(the_arity_of o) /. n = (the_arity_of o) . n
by A2, PARTFUN1:def 8;
A6:
(
dom (H1 . ((the_arity_of o) /. n)) = the
Sorts of
U1 . ((the_arity_of o) /. n) &
rng (H1 . ((the_arity_of o) /. n)) c= the
Sorts of
U2 . ((the_arity_of o) /. n) )
by FUNCT_2:def 1, RELAT_1:def 19;
dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))) = the
Sorts of
U1 . ((the_arity_of o) /. n)
by FUNCT_2:def 1;
then A7:
dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))) = dom (H1 . ((the_arity_of o) /. n))
by A6;
(the Sorts of U1 * (the_arity_of o)) . n = the
Sorts of
U1 . ((the_arity_of o) /. n)
by A2, A4, A5, FUNCT_1:22;
then A8:
x . n in dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n)))
by A2, A4, A6, A7, Th6;
(H2 ** H1) . ((the_arity_of o) /. n) = (H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))
by Th2;
hence ((H2 ** H1) # x) . y =
(H2 . ((the_arity_of o) /. n)) . ((H1 . ((the_arity_of o) /. n)) . (x . n))
by A3, A8, FUNCT_1:22
.=
(H2 . ((the_arity_of o) /. n)) . ((H1 # x) . n)
by A1, A2, Def8
.=
(H2 # (H1 # x)) . y
by A1, A2, Def8
;
:: thesis: verum
end;
hence
(H2 ** H1) # x = H2 # (H1 # x)
by A1, FUNCT_1:9; :: thesis: verum