let R be non degenerated comRing; :: thesis: for f, g being Element of (Polynom-Ring (1,R)) holds (BSPoly R) . (f * g) = ((BSPoly R) . f) * ((BSPoly R) . g)
let f, g be Element of (Polynom-Ring (1,R)); :: thesis: (BSPoly R) . (f * g) = ((BSPoly R) . f) * ((BSPoly R) . g)
set FS1 = Formal-Series (1,R);
set FS = Formal-Series R;
reconsider PR = Polynom-Ring R as Subring of Formal-Series R by Th35;
reconsider f0 = f, g0 = g as Element of (Formal-Series (1,R)) by Lm7, TARSKI:def 3;
A1: (BSPoly R) . f = (BSFSeri R) . f by FUNCT_1:49;
A2: (BSPoly R) . g = (BSFSeri R) . g by FUNCT_1:49;
A3: (BSPoly R) . (f * g) = (BSFSeri R) . (f * g) by FUNCT_1:49;
reconsider s = (BSFSeri R) . f0, t = (BSFSeri R) . g0 as Element of (Formal-Series R) ;
reconsider p = (BSPoly R) . f, q = (BSPoly R) . g as Element of PR ;
((BSPoly R) . f) * ((BSPoly R) . g) = p * q
.= s * t by A1, A2, Lm3
.= (BSFSeri R) . (f0 * g0) by Th29
.= (BSPoly R) . (f * g) by Th47, A3 ;
hence (BSPoly R) . (f * g) = ((BSPoly R) . f) * ((BSPoly R) . g) ; :: thesis: verum