let S be non empty non void ManySortedSign ; for A being MSAlgebra over S
for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A
let A be MSAlgebra over S; for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A
let h1, h2 be Endomorphism of A; h2 ** h1 is Endomorphism of A
let o be OperSymbol of S; MSUALG_3:def 7,MSUALG_6:def 2 ( Args (o,A) = {} or for b1 being Element of Args (o,A) holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,A)) . ((h2 ** h1) # b1) )
assume A1:
Args (o,A) <> {}
; for b1 being Element of Args (o,A) holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,A)) . ((h2 ** h1) # b1)
set h = h2 ** h1;
let x be Element of Args (o,A); ((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:3;
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 A7:
the
Sorts of
A . (the_result_sort_of o) <> {}
;
((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:5, FUNCT_2:15
.=
(h2 . (the_result_sort_of o)) . ((Den (o,A)) . (h1 # x))
by A4, A1
.=
(Den (o,A)) . (h2 # (h1 # x))
by A3, A1
;
hence
((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x)
by A1, Th5;
verum end;