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));
( (0_. L) +* 0 ,(- (1_ L)) is sequence of L & n in NAT ) ;
then A1: n in dom ((0_. L) +* 0 ,(- (1_ L))) by NORMSP_1:17;
set q = (0_. L) +* n,(1_ L);
A2: unital_poly L,n = ((0_. L) +* n,(1_ L)) +* 0 ,(- (1_ L)) by FUNCT_7:35;
( (0_. L) +* n,(1_ L) is sequence of L & 0 in NAT ) ;
then 0 in dom ((0_. L) +* n,(1_ L)) by NORMSP_1:17;
hence ( (unital_poly L,n) . 0 = - (1_ L) & (unital_poly L,n) . n = 1_ L ) by A1, A2, FUNCT_7:33; :: thesis: verum