let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S
for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A
let A be MSAlgebra of S; :: thesis: for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A
let h1, h2 be Endomorphism of A; :: thesis: h2 ** h1 is Endomorphism of A
A1: ( h1 is_homomorphism A,A & h2 is_homomorphism A,A ) by Def2;
let o be OperSymbol of S; :: according to MSUALG_3:def 9,MSUALG_6:def 2 :: thesis: ( Args o,A = {} or for b₁ being Element of Args o,A holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . b₁) = (Den o,A) . ((h2 ** h1) # b₁) )
assume A2: Args o,A <> {} ; :: thesis: for b₁ being Element of Args o,A holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . b₁) = (Den o,A) . ((h2 ** h1) # b₁)
let x be Element of Args o,A; :: thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = (Den o,A) . ((h2 ** h1) # x)
A3: Result o,A = the Sorts of A . (the_result_sort_of o) by PRALG_2:10;
set h = h2 ** h1;
reconsider f1 = h1 . (the_result_sort_of o), f2 = h2 . (the_result_sort_of o), f = (h2 ** h1) . (the_result_sort_of o) as Function of (the Sorts of A . (the_result_sort_of o)),(the Sorts of A . (the_result_sort_of o)) ;

per cases ( the Sorts of A . (the_result_sort_of o) = {} or the Sorts of A . (the_result_sort_of o) <> {} ) ;

suppose the Sorts of A . (the_result_sort_of o) = {} ; :: thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = (Den o,A) . ((h2 ** h1) # x)

then ( dom f = {} & Den o,A = {} ) by A3;
then ( f . ((Den o,A) . x) = {} & dom (Den o,A) = {} ) by FUNCT_1:def 4;
hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = (Den o,A) . ((h2 ** h1) # x) by FUNCT_1:def 4; :: thesis: verum

end;

suppose A4: the Sorts of A . (the_result_sort_of o) <> {} ; :: thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = (Den o,A) . ((h2 ** h1) # x)

(h2 ** h1) . (the_result_sort_of o) = f2 * f1 by MSUALG_3:2;
then ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = f2 . (f1 . ((Den o,A) . x)) by A2, A3, A4, FUNCT_2:7, FUNCT_2:21
.= (h2 . (the_result_sort_of o)) . ((Den o,A) . (h1 # x)) by A1, A2, MSUALG_3:def 9
.= (Den o,A) . (h2 # (h1 # x)) by A1, A2, MSUALG_3:def 9 ;
hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = (Den o,A) . ((h2 ** h1) # x) by A2, Th5; :: thesis: verum

end;

end;