let S be non empty non void ManySortedSign ; for U1 being MSAlgebra of S holds id the Sorts of U1 is_homomorphism U1,U1
let U1 be MSAlgebra of S; id the Sorts of U1 is_homomorphism U1,U1
set F = id the Sorts of U1;
let o be OperSymbol of S; MSUALG_3:def 9 ( 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 <> {}
; 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; ((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 4;
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 10, RELAT_1:46;
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: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 <> {}
;
((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 5, 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:35;
verum end;