defpred S₁[ object , object ] means ex x1 being Series of 1,R st
( x1 = $1 & $2 = x1 * NBag1 );
A1: for x being object st x in the carrier of (Formal-Series (1,R)) holds
ex y being object st
( y in the carrier of (Formal-Series R) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (Formal-Series (1,R)) implies ex y being object st
( y in the carrier of (Formal-Series R) & S₁[x,y] ) )
assume x in the carrier of (Formal-Series (1,R)) ; :: thesis: ex y being object st
( y in the carrier of (Formal-Series R) & S₁[x,y] )
then reconsider x1 = x as Series of 1,R by Def3;
take y = x1 * NBag1; :: thesis: ( y in the carrier of (Formal-Series R) & S₁[x,y] )
thus ( y in the carrier of (Formal-Series R) & S₁[x,y] ) by POLYALG1:def 2; :: thesis: verum

end;

ex g being Function of (Formal-Series (1,R)),(Formal-Series R) st
for x being object st x in the carrier of (Formal-Series (1,R)) holds
S₁[x,g . x] from FUNCT_2:sch 1(A1);
then consider g being Function of (Formal-Series (1,R)),(Formal-Series R) such that
A2: for x being object st x in the carrier of (Formal-Series (1,R)) holds
ex x1 being Series of 1,R st
( x1 = x & g . x = x1 * NBag1 ) ;
take g ; :: thesis: for x being object st x in the carrier of (Formal-Series (1,R)) holds
ex x1 being Series of 1,R st
( x1 = x & g . x = x1 * NBag1 )
thus for x being object st x in the carrier of (Formal-Series (1,R)) holds
ex x1 being Series of 1,R st
( x1 = x & g . x = x1 * NBag1 ) by A2; :: thesis: verum