let S be non empty non void ManySortedSign ; :: thesis: for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1
let U1 be MSAlgebra over 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 7 :: 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)
A2: (id the Sorts of U1) # x = x by A1, Th7;
set r = the_result_sort_of o;
A3: (id the Sorts of U1) . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) by Def1;
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 2;
then A4: ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def 5, RELAT_1:27;
o in the carrier' of S ;
then o in dom the ResultSort of S by FUNCT_2:def 1;
then A5: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A4, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;

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 dom (Den (o,U1)) = Args (o,U1) by FUNCT_2:def 1;
then ( rng (Den (o,U1)) c= Result (o,U1) & (Den (o,U1)) . x in rng (Den (o,U1)) ) by A1, FUNCT_1:def 3, RELAT_1:def 19;
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, A5, FUNCT_1:18; :: thesis: verum

end;

suppose A6: 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)) = {} ;
then A7: (Den (o,U1)) . x = {} by FUNCT_1:def 2;
dom ((id the Sorts of U1) . (the_result_sort_of o)) = {} by A5, A6;
then ((id the Sorts of U1) . (the_result_sort_of o)) . {} = {} by FUNCT_1:def 2;
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, A7, Th7; :: thesis: verum

end;

end;