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
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 A1: 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₁)
set h = h2 ** h1;
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)
A2: Result o,A = the Sorts of A . (the_result_sort_of o) by PRALG_2:10;
A3: h2 is_homomorphism A,A by Def2;
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)) ;
A4: h1 is_homomorphism A,A by Def2;

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

suppose A5: 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 = {} ;
then A6: f . ((Den o,A) . x) = {} by FUNCT_1:def 4;
dom (Den o,A) = {} by A2, A5;
hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = (Den o,A) . ((h2 ** h1) # x) by A6, FUNCT_1:def 4; :: thesis: verum

end;

suppose A7: 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 A1, A2, A7, FUNCT_2:7, FUNCT_2:21
.= (h2 . (the_result_sort_of o)) . ((Den o,A) . (h1 # x)) by A4, A1, MSUALG_3:def 9
.= (Den o,A) . (h2 # (h1 # x)) by A3, A1, MSUALG_3:def 9 ;
hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den o,A) . x) = (Den o,A) . ((h2 ** h1) # x) by A1, Th5; :: thesis: verum

end;

end;