set f = ((0_. F_Rat) +* (0,(- 2))) +* (3,1);
H: dom (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) = dom ((0_. F_Rat) +* (0,(- 2))) by FUNCT_7:30
.= dom (0_. F_Rat) by FUNCT_7:30
.= NAT ;

now :: thesis: for x being object st x in NAT holds
(((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . x in the carrier of F_Rat

let x be object ; :: thesis: ( x in NAT implies (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . b₁ in the carrier of F_Rat )
assume x in NAT ; :: thesis: (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . b₁ in the carrier of F_Rat
then reconsider i = x as Element of NAT ;
( i <= 3 implies not not i = 0 & ... & not i = 3 ) ;

per cases then ( i = 0 or i = 1 or i = 2 or i = 3 or i > 3 ) ;

suppose i = 0 ; :: thesis: (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . b₁ in the carrier of F_Rat

hence (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . x in the carrier of F_Rat by LL0, RAT_1:def 2, GAUSSINT:def 14; :: thesis: verum

end;

suppose i = 1 ; :: thesis: (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . b₁ in the carrier of F_Rat

hence (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . x in the carrier of F_Rat by LL0, GAUSSINT:def 14; :: thesis: verum

end;

suppose i = 2 ; :: thesis: (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . b₁ in the carrier of F_Rat

hence (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . x in the carrier of F_Rat by LL0, GAUSSINT:def 14; :: thesis: verum

end;

suppose i = 3 ; :: thesis: (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . b₁ in the carrier of F_Rat

hence (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . x in the carrier of F_Rat by LL0, GAUSSINT:def 14; :: thesis: verum

end;

suppose i > 3 ; :: thesis: (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . b₁ in the carrier of F_Rat

then i >= 3 + 1 by NAT_1:13;
then (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . i = 0. F_Rat by LL0, GAUSSINT:def 14;
hence (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . x in the carrier of F_Rat ; :: thesis: verum

end;

end;

end;

then reconsider f = ((0_. F_Rat) +* (0,(- 2))) +* (3,1) as sequence of the carrier of F_Rat by H, FUNCT_2:3;
f is finite-Support by LL0, GAUSSINT:def 14;
hence ((0_. F_Rat) +* (0,(- 2))) +* (3,1) is Element of the carrier of (Polynom-Ring F_Rat) by POLYNOM3:def 10; :: thesis: verum