let L be non empty left_unital doubleLoopStr ; :: thesis: for n being non zero Nat

for i being Nat st i <> 0 & i <> n holds

(unital_poly (L,n)) . i = 0. L

let n be non zero Nat; :: thesis: for i being Nat st i <> 0 & i <> n holds

(unital_poly (L,n)) . i = 0. L

let i be Nat; :: thesis: ( i <> 0 & i <> n implies (unital_poly (L,n)) . i = 0. L )

assume that

A1: i <> 0 and

A2: i <> n ; :: thesis: (unital_poly (L,n)) . i = 0. L

set p = (0_. L) +* (0,(- (1_ L)));

A3: i in NAT by ORDINAL1:def 12;

(((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = ((0_. L) +* (0,(- (1_ L)))) . i by A2, FUNCT_7:32

.= (0_. L) . i by A1, FUNCT_7:32

.= 0. L by A3, FUNCOP_1:7 ;

hence (unital_poly (L,n)) . i = 0. L ; :: thesis: verum

for i being Nat st i <> 0 & i <> n holds

(unital_poly (L,n)) . i = 0. L

let n be non zero Nat; :: thesis: for i being Nat st i <> 0 & i <> n holds

(unital_poly (L,n)) . i = 0. L

let i be Nat; :: thesis: ( i <> 0 & i <> n implies (unital_poly (L,n)) . i = 0. L )

assume that

A1: i <> 0 and

A2: i <> n ; :: thesis: (unital_poly (L,n)) . i = 0. L

set p = (0_. L) +* (0,(- (1_ L)));

A3: i in NAT by ORDINAL1:def 12;

(((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = ((0_. L) +* (0,(- (1_ L)))) . i by A2, FUNCT_7:32

.= (0_. L) . i by A1, FUNCT_7:32

.= 0. L by A3, FUNCOP_1:7 ;

hence (unital_poly (L,n)) . i = 0. L ; :: thesis: verum