set FS1 = Formal-Series (1,R);
set FS = Formal-Series R;
let f, g be Function of (Formal-Series (1,R)),(Formal-Series R); :: 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 & f . x = x1 * NBag1 ) ) & ( 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 ) ) implies f = g )
assume that
A3: 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 & f . x = x1 * NBag1 ) and
A4: 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 ) ; :: thesis: f = g

now :: thesis: for x being object st x in the carrier of (Formal-Series (1,R)) holds
f . x = g . x

let x be object ; :: thesis: ( x in the carrier of (Formal-Series (1,R)) implies f . x = g . x )
assume A5: x in the carrier of (Formal-Series (1,R)) ; :: thesis: f . x = g . x
then consider x1 being Series of 1,R such that
A6: ( x1 = x & f . x = x1 * NBag1 ) by A3;
consider x2 being Series of 1,R such that
A7: ( x2 = x & g . x = x2 * NBag1 ) by A4, A5;
f . x = x2 * NBag1 by A6, A7
.= g . x by A7 ;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g ; :: thesis: verum