let L be non empty left_unital doubleLoopStr ; :: thesis: for n being non zero Element of NAT holds
( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L )
let n be non zero Element of NAT ; :: thesis: ( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L )
set p = (0_. L) +* (0,(- (1_ L)));
set q = (0_. L) +* (n,(1_ L));
0 in NAT ;
then A1: ( unital_poly (L,n) = ((0_. L) +* (n,(1_ L))) +* (0,(- (1_ L))) & 0 in dom ((0_. L) +* (n,(1_ L))) ) by FUNCT_7:33, NORMSP_1:12;
n in NAT ;
then n in dom ((0_. L) +* (0,(- (1_ L)))) by NORMSP_1:12;
hence ( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L ) by A1, FUNCT_7:31; :: thesis: verum