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 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 13;
(((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = ((0_. L) +* 0 ,(- (1_ L))) . i by A2, FUNCT_7:34
.= (0_. L) . i by A1, FUNCT_7:34
.= 0. L by A3, FUNCOP_1:13 ;
hence (unital_poly L,n) . i = 0. L ; :: thesis: verum