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