let L be non empty left_unital doubleLoopStr ; :: thesis: for n being non empty Element of NAT holds
( (unital_poly L,n) . 0 = - (1_ L) & (unital_poly L,n) . n = 1_ L )
let n be non empty 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:35, NORMSP_1:17;
n in NAT ;
then n in dom ((0_. L) +* 0 ,(- (1_ L))) by NORMSP_1:17;
hence ( (unital_poly L,n) . 0 = - (1_ L) & (unital_poly L,n) . n = 1_ L ) by A1, FUNCT_7:33; :: thesis: verum