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

( (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