let L be non empty left_unital doubleLoopStr ; :: thesis: for n being non empty Nat
for i being Nat st i <> 0 & i <> n holds
(unital_poly L,n) . i = 0. L
let n be non empty 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 A1: ( i <> 0 & i <> n ) ; :: thesis: (unital_poly L,n) . i = 0. L
A2: i in NAT by ORDINAL1:def 13;
set p = (0_. L) +* 0 ,(- (1_ L));
(((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = ((0_. L) +* 0 ,(- (1_ L))) . i by A1, FUNCT_7:34
.= (0_. L) . i by A1, FUNCT_7:34
.= 0. L by A2, FUNCOP_1:13 ;
hence (unital_poly L,n) . i = 0. L ; :: thesis: verum