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 ;

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) = {} )
;

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)) = 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;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

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;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