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) . ) . ((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) . ) . ((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) . ) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x)
A2: (id the Sorts of U1) # x = x by ;
set r = the_result_sort_of o;
A3: (id the Sorts of U1) . = id ( the Sorts of U1 . ) 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 ;
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
.= the Sorts of U1 . by MSUALG_1:def 2 ;
per cases ( Result (o,U1) <> {} or Result (o,U1) = {} ) ;
suppose Result (o,U1) <> {} ; :: thesis: ((id the Sorts of U1) . ) . ((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 ;
hence ((id the Sorts of U1) . ) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) by ; :: thesis: verum
end;
suppose A6: Result (o,U1) = {} ; :: thesis: ((id the Sorts of U1) . ) . ((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) . ) = {} by A5, A6;
then ((id the Sorts of U1) . ) . {} = {} by FUNCT_1:def 2;
hence ((id the Sorts of U1) . ) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) by A1, A7, Th7; :: thesis: verum
end;
end;