set L = F_Rat ;
set f = ((0_. F_Rat) +* (0,(- 2))) +* (3,1);
A1: 0 in dom (0_. F_Rat) ;
thus (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 0 = ((0_. F_Rat) +* (0,(- 2))) . 0 by FUNCT_7:32
.= - 2 by A1, FUNCT_7:31 ; :: thesis: ( (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 1 = 0 & (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 2 = 0 & (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 3 = 1 & ( for n being Nat st n >= 4 holds
(((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = 0 ) )
thus (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 1 = ((0_. F_Rat) +* (0,(- 2))) . 1 by FUNCT_7:32
.= (0_. F_Rat) . 1 by FUNCT_7:32
.= 0 by GAUSSINT:def 14 ; :: thesis: ( (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 2 = 0 & (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 3 = 1 & ( for n being Nat st n >= 4 holds
(((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = 0 ) )
thus (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 2 = ((0_. F_Rat) +* (0,(- 2))) . 2 by FUNCT_7:32
.= (0_. F_Rat) . 2 by FUNCT_7:32
.= 0 by GAUSSINT:def 14 ; :: thesis: ( (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 3 = 1 & ( for n being Nat st n >= 4 holds
(((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = 0 ) )
( 3 in NAT & dom ((0_. F_Rat) +* (0,(- 2))) = dom (0_. F_Rat) ) by FUNCT_7:30;
hence (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 3 = 1 by FUNCT_7:31; :: thesis: for n being Nat st n >= 4 holds
(((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = 0
let n be Nat; :: thesis: ( n >= 4 implies (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = 0 )
assume A4: n >= 4 ; :: thesis: (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = 0
then n >= ((1 + 1) + 1) + 1 ;
then n > ((0 + 1) + 1) + 1 by NAT_1:13;
hence (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = ((0_. F_Rat) +* (0,(- 2))) . n by FUNCT_7:32
.= (0_. F_Rat) . n by A4, FUNCT_7:32
.= 0 by ORDINAL1:def 12, FUNCOP_1:7, GAUSSINT:def 14 ;
:: thesis: verum