let R be non degenerated comRing; SBFSeri R is RingHomomorphism
set P = BSFSeri R;
set FS1 = Formal-Series (1,R);
set FS = Formal-Series R;
A1:
BSFSeri R is onto
;
A2:
( BSFSeri R is additive & BSFSeri R is multiplicative & BSFSeri R is unity-preserving )
;
A3:
for x, y being Element of (Formal-Series R) holds
( ((BSFSeri R) ") . (x + y) = (((BSFSeri R) ") . x) + (((BSFSeri R) ") . y) & ((BSFSeri R) ") . (x * y) = (((BSFSeri R) ") . x) * (((BSFSeri R) ") . y) & ((BSFSeri R) ") . (1_ (Formal-Series R)) = 1_ (Formal-Series (1,R)) )
proof
A4:
((BSFSeri R) ") . (1_ (Formal-Series R)) =
((BSFSeri R) ") . ((BSFSeri R) . (1_ (Formal-Series (1,R))))
by GROUP_1:def 13
.=
1_ (Formal-Series (1,R))
by FUNCT_2:26
;
let x,
y be
Element of
(Formal-Series R);
( ((BSFSeri R) ") . (x + y) = (((BSFSeri R) ") . x) + (((BSFSeri R) ") . y) & ((BSFSeri R) ") . (x * y) = (((BSFSeri R) ") . x) * (((BSFSeri R) ") . y) & ((BSFSeri R) ") . (1_ (Formal-Series R)) = 1_ (Formal-Series (1,R)) )
consider x9 being
object such that A5:
x9 in the
carrier of
(Formal-Series (1,R))
and A6:
(BSFSeri R) . x9 = x
by A1, FUNCT_2:11;
reconsider x9 =
x9 as
Element of
(Formal-Series (1,R)) by A5;
A7:
x9 =
((BSFSeri R) ") . ((BSFSeri R) . x9)
by FUNCT_2:26
.=
((BSFSeri R) ") . x
by A6
;
consider y9 being
object such that A8:
y9 in the
carrier of
(Formal-Series (1,R))
and A9:
(BSFSeri R) . y9 = y
by A1, FUNCT_2:11;
reconsider y9 =
y9 as
Element of
(Formal-Series (1,R)) by A8;
A10:
y9 =
((BSFSeri R) ") . ((BSFSeri R) . y9)
by FUNCT_2:26
.=
((BSFSeri R) ") . y
by A9
;
A11:
((BSFSeri R) ") . (x * y) =
((BSFSeri R) ") . ((BSFSeri R) . (x9 * y9))
by A2, A6, A9
.=
((BSFSeri R) ") . ((BSFSeri R) . (x9 * y9))
.=
(((BSFSeri R) ") . x) * (((BSFSeri R) ") . y)
by A7, A10, FUNCT_2:26
;
((BSFSeri R) ") . (x + y) =
((BSFSeri R) ") . ((BSFSeri R) . (x9 + y9))
by A2, A6, A9
.=
((BSFSeri R) ") . ((BSFSeri R) . (x9 + y9))
.=
(((BSFSeri R) ") . x) + (((BSFSeri R) ") . y)
by A7, A10, FUNCT_2:26
;
hence
(
((BSFSeri R) ") . (x + y) = (((BSFSeri R) ") . x) + (((BSFSeri R) ") . y) &
((BSFSeri R) ") . (x * y) = (((BSFSeri R) ") . x) * (((BSFSeri R) ") . y) &
((BSFSeri R) ") . (1_ (Formal-Series R)) = 1_ (Formal-Series (1,R)) )
by A11, A4;
verum
end;
( (BSFSeri R) " is additive & (BSFSeri R) " is multiplicative & (BSFSeri R) " is unity-preserving )
by A3;
hence
SBFSeri R is RingHomomorphism
by Th32; verum