let S be non empty non void ManySortedSign ; :: thesis: for U1 being MSAlgebra of S holds id the Sorts of U1 is_homomorphism U1,U1
let U1 be MSAlgebra of S; :: thesis: id the Sorts of U1 is_homomorphism U1,U1
set F = id the Sorts of U1;
let o be OperSymbol of S; :: according to MSUALG_3:def 9 :: thesis: ( Args o,U1 <> {} implies for x being Element of Args o,U1 holds ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U1) . ((id the Sorts of U1) # x) )
assume A1: Args o,U1 <> {} ; :: thesis: for x being Element of Args o,U1 holds ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U1) . ((id the Sorts of U1) # x)
let x be Element of Args o,U1; :: thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U1) . ((id the Sorts of U1) # x)
set r = the_result_sort_of o;
A2: (id the Sorts of U1) # x = x by A1, Th7;
A3: (id the Sorts of U1) . (the_result_sort_of o) = id (the Sorts of U1 . (the_result_sort_of o)) by Def1;
A4: Result o,U1 = (the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def 10;
rng the ResultSort of S c= the carrier of S by RELAT_1:def 19;
then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def 4;
then A5: dom (the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by RELAT_1:46;
o in the carrier' of S ;
then o in dom the ResultSort of S by FUNCT_2:def 1;
then A6: Result o,U1 = the Sorts of U1 . (the ResultSort of S . o) by A4, A5, FUNCT_1:22
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 7 ;

per cases ( Result o,U1 <> {} or Result o,U1 = {} ) ;

suppose Result o,U1 <> {} ; :: thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U1) . ((id the Sorts of U1) # x)

then A7: ( dom (Den o,U1) = Args o,U1 & rng (Den o,U1) c= Result o,U1 ) by FUNCT_2:def 1, RELAT_1:def 19;
then (Den o,U1) . x in rng (Den o,U1) by A1, FUNCT_1:def 5;
hence ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U1) . ((id the Sorts of U1) # x) by A2, A3, A6, A7, FUNCT_1:35; :: thesis: verum

end;

suppose Result o,U1 = {} ; :: thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U1) . ((id the Sorts of U1) # x)

then ( dom (Den o,U1) = {} & dom ((id the Sorts of U1) . (the_result_sort_of o)) = {} ) by A6;
then ( (Den o,U1) . x = {} & ((id the Sorts of U1) . (the_result_sort_of o)) . {} = {} ) by FUNCT_1:def 4;
hence ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U1) . ((id the Sorts of U1) # x) by A1, Th7; :: thesis: verum

end;

end;