:: ANPROJ_2 semantic presentation

REAL is non empty V35() set

NAT is non empty V17() V18() V19() Element of K32(REAL)

K32(REAL) is non empty set

NAT is non empty V17() V18() V19() set

K32(NAT) is non empty set

K32(NAT) is non empty set

COMPLEX is non empty V35() set

RAT is non empty V35() set

INT is non empty V35() set

K33(COMPLEX,COMPLEX) is non empty set

K32(K33(COMPLEX,COMPLEX)) is non empty set

K33(K33(COMPLEX,COMPLEX),COMPLEX) is non empty set

K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is non empty set

K33(REAL,REAL) is non empty set

K32(K33(REAL,REAL)) is non empty set

K33(K33(REAL,REAL),REAL) is non empty set

K32(K33(K33(REAL,REAL),REAL)) is non empty set

K33(RAT,RAT) is non empty set

K32(K33(RAT,RAT)) is non empty set

K33(K33(RAT,RAT),RAT) is non empty set

K32(K33(K33(RAT,RAT),RAT)) is non empty set

K33(INT,INT) is non empty set

K32(K33(INT,INT)) is non empty set

K33(K33(INT,INT),INT) is non empty set

K32(K33(K33(INT,INT),INT)) is non empty set

K33(NAT,NAT) is non empty set

K33(K33(NAT,NAT),NAT) is non empty set

K32(K33(K33(NAT,NAT),NAT)) is non empty set

{} is empty V17() V18() V19() V21() V22() V23() V24() V25() set

1 is non empty V17() V18() V19() V23() V24() V25() Element of NAT

0 is empty V17() V18() V19() V21() V22() V23() V24() V25() Element of NAT

- 1 is V24() V25() Element of REAL

K107(0) is V24() V25() set

CS is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the U1 of CS is non empty set

0. CS is zero Element of the U1 of CS

the U2 of CS is Element of the U1 of CS

p is Element of the U1 of CS

p1 is Element of the U1 of CS

p2 is Element of the U1 of CS

(0. CS) + (0. CS) is Element of the U1 of CS

the U5 of CS is V7() V10(K33( the U1 of CS, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS))

K33( the U1 of CS, the U1 of CS) is non empty set

K33(K33( the U1 of CS, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS)) is non empty set

K142( the U1 of CS, the U5 of CS,(0. CS),(0. CS)) is Element of the U1 of CS

K4((0. CS),(0. CS)) is set

the U5 of CS . K4((0. CS),(0. CS)) is set

((0. CS) + (0. CS)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((0. CS) + (0. CS)),(0. CS)) is Element of the U1 of CS

K4(((0. CS) + (0. CS)),(0. CS)) is set

the U5 of CS . K4(((0. CS) + (0. CS)),(0. CS)) is set

1 * p1 is Element of the U1 of CS

the Mult of CS is V7() V10(K33(REAL, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33(REAL, the U1 of CS), the U1 of CS))

K33(REAL, the U1 of CS) is non empty set

K33(K33(REAL, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33(REAL, the U1 of CS), the U1 of CS)) is non empty set

K138( the Mult of CS,1,p1) is set

K4(1,p1) is set

the Mult of CS . K4(1,p1) is set

(0. CS) + (1 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0. CS),(1 * p1)) is Element of the U1 of CS

K4((0. CS),(1 * p1)) is set

the U5 of CS . K4((0. CS),(1 * p1)) is set

((0. CS) + (1 * p1)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((0. CS) + (1 * p1)),(0. CS)) is Element of the U1 of CS

K4(((0. CS) + (1 * p1)),(0. CS)) is set

the U5 of CS . K4(((0. CS) + (1 * p1)),(0. CS)) is set

0 * p is Element of the U1 of CS

K138( the Mult of CS,0,p) is set

K4(0,p) is set

the Mult of CS . K4(0,p) is set

(0 * p) + (1 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0 * p),(1 * p1)) is Element of the U1 of CS

K4((0 * p),(1 * p1)) is set

the U5 of CS . K4((0 * p),(1 * p1)) is set

((0 * p) + (1 * p1)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((0 * p) + (1 * p1)),(0. CS)) is Element of the U1 of CS

K4(((0 * p) + (1 * p1)),(0. CS)) is set

the U5 of CS . K4(((0 * p) + (1 * p1)),(0. CS)) is set

0 * p2 is Element of the U1 of CS

K138( the Mult of CS,0,p2) is set

K4(0,p2) is set

the Mult of CS . K4(0,p2) is set

((0 * p) + (1 * p1)) + (0 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((0 * p) + (1 * p1)),(0 * p2)) is Element of the U1 of CS

K4(((0 * p) + (1 * p1)),(0 * p2)) is set

the U5 of CS . K4(((0 * p) + (1 * p1)),(0 * p2)) is set

1 * p2 is Element of the U1 of CS

K138( the Mult of CS,1,p2) is set

K4(1,p2) is set

the Mult of CS . K4(1,p2) is set

((0. CS) + (0. CS)) + (1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((0. CS) + (0. CS)),(1 * p2)) is Element of the U1 of CS

K4(((0. CS) + (0. CS)),(1 * p2)) is set

the U5 of CS . K4(((0. CS) + (0. CS)),(1 * p2)) is set

(0 * p) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0 * p),(0. CS)) is Element of the U1 of CS

K4((0 * p),(0. CS)) is set

the U5 of CS . K4((0 * p),(0. CS)) is set

((0 * p) + (0. CS)) + (1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((0 * p) + (0. CS)),(1 * p2)) is Element of the U1 of CS

K4(((0 * p) + (0. CS)),(1 * p2)) is set

the U5 of CS . K4(((0 * p) + (0. CS)),(1 * p2)) is set

0 * p1 is Element of the U1 of CS

K138( the Mult of CS,0,p1) is set

K4(0,p1) is set

the Mult of CS . K4(0,p1) is set

(0 * p) + (0 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0 * p),(0 * p1)) is Element of the U1 of CS

K4((0 * p),(0 * p1)) is set

the U5 of CS . K4((0 * p),(0 * p1)) is set

((0 * p) + (0 * p1)) + (1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((0 * p) + (0 * p1)),(1 * p2)) is Element of the U1 of CS

K4(((0 * p) + (0 * p1)),(1 * p2)) is set

the U5 of CS . K4(((0 * p) + (0 * p1)),(1 * p2)) is set

1 * p is Element of the U1 of CS

K138( the Mult of CS,1,p) is set

K4(1,p) is set

the Mult of CS . K4(1,p) is set

(1 * p) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * p),(0. CS)) is Element of the U1 of CS

K4((1 * p),(0. CS)) is set

the U5 of CS . K4((1 * p),(0. CS)) is set

((1 * p) + (0. CS)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((1 * p) + (0. CS)),(0. CS)) is Element of the U1 of CS

K4(((1 * p) + (0. CS)),(0. CS)) is set

the U5 of CS . K4(((1 * p) + (0. CS)),(0. CS)) is set

(1 * p) + (0 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * p),(0 * p1)) is Element of the U1 of CS

K4((1 * p),(0 * p1)) is set

the U5 of CS . K4((1 * p),(0 * p1)) is set

((1 * p) + (0 * p1)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((1 * p) + (0 * p1)),(0. CS)) is Element of the U1 of CS

K4(((1 * p) + (0 * p1)),(0. CS)) is set

the U5 of CS . K4(((1 * p) + (0 * p1)),(0. CS)) is set

((1 * p) + (0 * p1)) + (0 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((1 * p) + (0 * p1)),(0 * p2)) is Element of the U1 of CS

K4(((1 * p) + (0 * p1)),(0 * p2)) is set

the U5 of CS . K4(((1 * p) + (0 * p1)),(0 * p2)) is set

CS is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the U1 of CS is non empty set

0. CS is zero Element of the U1 of CS

the U2 of CS is Element of the U1 of CS

p is Element of the U1 of CS

p1 is Element of the U1 of CS

(0. CS) + (0. CS) is Element of the U1 of CS

the U5 of CS is V7() V10(K33( the U1 of CS, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS))

K33( the U1 of CS, the U1 of CS) is non empty set

K33(K33( the U1 of CS, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS)) is non empty set

K142( the U1 of CS, the U5 of CS,(0. CS),(0. CS)) is Element of the U1 of CS

K4((0. CS),(0. CS)) is set

the U5 of CS . K4((0. CS),(0. CS)) is set

1 * p1 is Element of the U1 of CS

the Mult of CS is V7() V10(K33(REAL, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33(REAL, the U1 of CS), the U1 of CS))

K33(REAL, the U1 of CS) is non empty set

K33(K33(REAL, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33(REAL, the U1 of CS), the U1 of CS)) is non empty set

K138( the Mult of CS,1,p1) is set

K4(1,p1) is set

the Mult of CS . K4(1,p1) is set

(0. CS) + (1 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0. CS),(1 * p1)) is Element of the U1 of CS

K4((0. CS),(1 * p1)) is set

the U5 of CS . K4((0. CS),(1 * p1)) is set

0 * p is Element of the U1 of CS

K138( the Mult of CS,0,p) is set

K4(0,p) is set

the Mult of CS . K4(0,p) is set

(0 * p) + (1 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0 * p),(1 * p1)) is Element of the U1 of CS

K4((0 * p),(1 * p1)) is set

the U5 of CS . K4((0 * p),(1 * p1)) is set

1 * p is Element of the U1 of CS

K138( the Mult of CS,1,p) is set

K4(1,p) is set

the Mult of CS . K4(1,p) is set

(1 * p) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * p),(0. CS)) is Element of the U1 of CS

K4((1 * p),(0. CS)) is set

the U5 of CS . K4((1 * p),(0. CS)) is set

0 * p1 is Element of the U1 of CS

K138( the Mult of CS,0,p1) is set

K4(0,p1) is set

the Mult of CS . K4(0,p1) is set

(1 * p) + (0 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * p),(0 * p1)) is Element of the U1 of CS

K4((1 * p),(0 * p1)) is set

the U5 of CS . K4((1 * p),(0 * p1)) is set

p2 is V24() V25() Element of REAL

p2 * p is Element of the U1 of CS

K138( the Mult of CS,p2,p) is set

K4(p2,p) is set

the Mult of CS . K4(p2,p) is set

r is V24() V25() Element of REAL

r * p1 is Element of the U1 of CS

K138( the Mult of CS,r,p1) is set

K4(r,p1) is set

the Mult of CS . K4(r,p1) is set

(p2 * p) - (r * p1) is Element of the U1 of CS

- (r * p1) is Element of the U1 of CS

K176(CS,(p2 * p),(- (r * p1))) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p2 * p),(- (r * p1))) is Element of the U1 of CS

K4((p2 * p),(- (r * p1))) is set

the U5 of CS . K4((p2 * p),(- (r * p1))) is set

- p1 is Element of the U1 of CS

r * (- p1) is Element of the U1 of CS

K138( the Mult of CS,r,(- p1)) is set

K4(r,(- p1)) is set

the Mult of CS . K4(r,(- p1)) is set

(p2 * p) + (r * (- p1)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p2 * p),(r * (- p1))) is Element of the U1 of CS

K4((p2 * p),(r * (- p1))) is set

the U5 of CS . K4((p2 * p),(r * (- p1))) is set

- r is V24() V25() Element of REAL

(- r) * p1 is Element of the U1 of CS

K138( the Mult of CS,(- r),p1) is set

K4((- r),p1) is set

the Mult of CS . K4((- r),p1) is set

(p2 * p) + ((- r) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p2 * p),((- r) * p1)) is Element of the U1 of CS

K4((p2 * p),((- r) * p1)) is set

the U5 of CS . K4((p2 * p),((- r) * p1)) is set

CS is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the U1 of CS is non empty set

0. CS is zero Element of the U1 of CS

the U2 of CS is Element of the U1 of CS

p is Element of the U1 of CS

p1 is Element of the U1 of CS

p2 is Element of the U1 of CS

r is Element of the U1 of CS

r1 is V24() V25() Element of REAL

r1 * p is Element of the U1 of CS

the Mult of CS is V7() V10(K33(REAL, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33(REAL, the U1 of CS), the U1 of CS))

K33(REAL, the U1 of CS) is non empty set

K33(K33(REAL, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33(REAL, the U1 of CS), the U1 of CS)) is non empty set

K138( the Mult of CS,r1,p) is set

K4(r1,p) is set

the Mult of CS . K4(r1,p) is set

p is V24() V25() Element of REAL

p * p1 is Element of the U1 of CS

K138( the Mult of CS,p,p1) is set

K4(p,p1) is set

the Mult of CS . K4(p,p1) is set

(r1 * p) + (p * p1) is Element of the U1 of CS

the U5 of CS is V7() V10(K33( the U1 of CS, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS))

K33( the U1 of CS, the U1 of CS) is non empty set

K33(K33( the U1 of CS, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS)) is non empty set

K142( the U1 of CS, the U5 of CS,(r1 * p),(p * p1)) is Element of the U1 of CS

K4((r1 * p),(p * p1)) is set

the U5 of CS . K4((r1 * p),(p * p1)) is set

p1 is V24() V25() Element of REAL

p1 * p2 is Element of the U1 of CS

K138( the Mult of CS,p1,p2) is set

K4(p1,p2) is set

the Mult of CS . K4(p1,p2) is set

((r1 * p) + (p * p1)) + (p1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((r1 * p) + (p * p1)),(p1 * p2)) is Element of the U1 of CS

K4(((r1 * p) + (p * p1)),(p1 * p2)) is set

the U5 of CS . K4(((r1 * p) + (p * p1)),(p1 * p2)) is set

(((r1 * p) + (p * p1)) + (p1 * p2)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((r1 * p) + (p * p1)) + (p1 * p2)),(0. CS)) is Element of the U1 of CS

K4((((r1 * p) + (p * p1)) + (p1 * p2)),(0. CS)) is set

the U5 of CS . K4((((r1 * p) + (p * p1)) + (p1 * p2)),(0. CS)) is set

0 * r is Element of the U1 of CS

K138( the Mult of CS,0,r) is set

K4(0,r) is set

the Mult of CS . K4(0,r) is set

(((r1 * p) + (p * p1)) + (p1 * p2)) + (0 * r) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((r1 * p) + (p * p1)) + (p1 * p2)),(0 * r)) is Element of the U1 of CS

K4((((r1 * p) + (p * p1)) + (p1 * p2)),(0 * r)) is set

the U5 of CS . K4((((r1 * p) + (p * p1)) + (p1 * p2)),(0 * r)) is set

r1 is V24() V25() Element of REAL

r1 * p2 is Element of the U1 of CS

K138( the Mult of CS,r1,p2) is set

K4(r1,p2) is set

the Mult of CS . K4(r1,p2) is set

p is V24() V25() Element of REAL

p * r is Element of the U1 of CS

K138( the Mult of CS,p,r) is set

K4(p,r) is set

the Mult of CS . K4(p,r) is set

(r1 * p2) + (p * r) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r1 * p2),(p * r)) is Element of the U1 of CS

K4((r1 * p2),(p * r)) is set

the U5 of CS . K4((r1 * p2),(p * r)) is set

p1 is V24() V25() Element of REAL

p1 * p is Element of the U1 of CS

K138( the Mult of CS,p1,p) is set

K4(p1,p) is set

the Mult of CS . K4(p1,p) is set

((r1 * p2) + (p * r)) + (p1 * p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((r1 * p2) + (p * r)),(p1 * p)) is Element of the U1 of CS

K4(((r1 * p2) + (p * r)),(p1 * p)) is set

the U5 of CS . K4(((r1 * p2) + (p * r)),(p1 * p)) is set

(p1 * p) + (r1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p1 * p),(r1 * p2)) is Element of the U1 of CS

K4((p1 * p),(r1 * p2)) is set

the U5 of CS . K4((p1 * p),(r1 * p2)) is set

((p1 * p) + (r1 * p2)) + (p * r) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((p1 * p) + (r1 * p2)),(p * r)) is Element of the U1 of CS

K4(((p1 * p) + (r1 * p2)),(p * r)) is set

the U5 of CS . K4(((p1 * p) + (r1 * p2)),(p * r)) is set

(p1 * p) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p1 * p),(0. CS)) is Element of the U1 of CS

K4((p1 * p),(0. CS)) is set

the U5 of CS . K4((p1 * p),(0. CS)) is set

((p1 * p) + (0. CS)) + (r1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((p1 * p) + (0. CS)),(r1 * p2)) is Element of the U1 of CS

K4(((p1 * p) + (0. CS)),(r1 * p2)) is set

the U5 of CS . K4(((p1 * p) + (0. CS)),(r1 * p2)) is set

(((p1 * p) + (0. CS)) + (r1 * p2)) + (p * r) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((p1 * p) + (0. CS)) + (r1 * p2)),(p * r)) is Element of the U1 of CS

K4((((p1 * p) + (0. CS)) + (r1 * p2)),(p * r)) is set

the U5 of CS . K4((((p1 * p) + (0. CS)) + (r1 * p2)),(p * r)) is set

0 * p1 is Element of the U1 of CS

K138( the Mult of CS,0,p1) is set

K4(0,p1) is set

the Mult of CS . K4(0,p1) is set

(p1 * p) + (0 * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p1 * p),(0 * p1)) is Element of the U1 of CS

K4((p1 * p),(0 * p1)) is set

the U5 of CS . K4((p1 * p),(0 * p1)) is set

((p1 * p) + (0 * p1)) + (r1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((p1 * p) + (0 * p1)),(r1 * p2)) is Element of the U1 of CS

K4(((p1 * p) + (0 * p1)),(r1 * p2)) is set

the U5 of CS . K4(((p1 * p) + (0 * p1)),(r1 * p2)) is set

(((p1 * p) + (0 * p1)) + (r1 * p2)) + (p * r) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((p1 * p) + (0 * p1)) + (r1 * p2)),(p * r)) is Element of the U1 of CS

K4((((p1 * p) + (0 * p1)) + (r1 * p2)),(p * r)) is set

the U5 of CS . K4((((p1 * p) + (0 * p1)) + (r1 * p2)),(p * r)) is set

CS is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the U1 of CS is non empty set

p is Element of the U1 of CS

p1 is Element of the U1 of CS

p2 is Element of the U1 of CS

r is V24() V25() Element of REAL

r1 is V24() V25() Element of REAL

r1 * p is Element of the U1 of CS

the Mult of CS is V7() V10(K33(REAL, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33(REAL, the U1 of CS), the U1 of CS))

K33(REAL, the U1 of CS) is non empty set

K33(K33(REAL, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33(REAL, the U1 of CS), the U1 of CS)) is non empty set

K138( the Mult of CS,r1,p) is set

K4(r1,p) is set

the Mult of CS . K4(r1,p) is set

r * r1 is V24() V25() Element of REAL

(r * r1) * p is Element of the U1 of CS

K138( the Mult of CS,(r * r1),p) is set

K4((r * r1),p) is set

the Mult of CS . K4((r * r1),p) is set

p is V24() V25() Element of REAL

p * p1 is Element of the U1 of CS

K138( the Mult of CS,p,p1) is set

K4(p,p1) is set

the Mult of CS . K4(p,p1) is set

(r1 * p) + (p * p1) is Element of the U1 of CS

the U5 of CS is V7() V10(K33( the U1 of CS, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS))

K33( the U1 of CS, the U1 of CS) is non empty set

K33(K33( the U1 of CS, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS)) is non empty set

K142( the U1 of CS, the U5 of CS,(r1 * p),(p * p1)) is Element of the U1 of CS

K4((r1 * p),(p * p1)) is set

the U5 of CS . K4((r1 * p),(p * p1)) is set

r * p is V24() V25() Element of REAL

(r * p) * p1 is Element of the U1 of CS

K138( the Mult of CS,(r * p),p1) is set

K4((r * p),p1) is set

the Mult of CS . K4((r * p),p1) is set

((r * r1) * p) + ((r * p) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((r * r1) * p),((r * p) * p1)) is Element of the U1 of CS

K4(((r * r1) * p),((r * p) * p1)) is set

the U5 of CS . K4(((r * r1) * p),((r * p) * p1)) is set

p1 is V24() V25() Element of REAL

p1 * p2 is Element of the U1 of CS

K138( the Mult of CS,p1,p2) is set

K4(p1,p2) is set

the Mult of CS . K4(p1,p2) is set

((r1 * p) + (p * p1)) + (p1 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((r1 * p) + (p * p1)),(p1 * p2)) is Element of the U1 of CS

K4(((r1 * p) + (p * p1)),(p1 * p2)) is set

the U5 of CS . K4(((r1 * p) + (p * p1)),(p1 * p2)) is set

r * (((r1 * p) + (p * p1)) + (p1 * p2)) is Element of the U1 of CS

K138( the Mult of CS,r,(((r1 * p) + (p * p1)) + (p1 * p2))) is set

K4(r,(((r1 * p) + (p * p1)) + (p1 * p2))) is set

the Mult of CS . K4(r,(((r1 * p) + (p * p1)) + (p1 * p2))) is set

r * p1 is V24() V25() Element of REAL

(r * p1) * p2 is Element of the U1 of CS

K138( the Mult of CS,(r * p1),p2) is set

K4((r * p1),p2) is set

the Mult of CS . K4((r * p1),p2) is set

(((r * r1) * p) + ((r * p) * p1)) + ((r * p1) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((r * r1) * p) + ((r * p) * p1)),((r * p1) * p2)) is Element of the U1 of CS

K4((((r * r1) * p) + ((r * p) * p1)),((r * p1) * p2)) is set

the U5 of CS . K4((((r * r1) * p) + ((r * p) * p1)),((r * p1) * p2)) is set

r * (r1 * p) is Element of the U1 of CS

K138( the Mult of CS,r,(r1 * p)) is set

K4(r,(r1 * p)) is set

the Mult of CS . K4(r,(r1 * p)) is set

(r * (r1 * p)) + ((r * p) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r * (r1 * p)),((r * p) * p1)) is Element of the U1 of CS

K4((r * (r1 * p)),((r * p) * p1)) is set

the U5 of CS . K4((r * (r1 * p)),((r * p) * p1)) is set

((r * (r1 * p)) + ((r * p) * p1)) + ((r * p1) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((r * (r1 * p)) + ((r * p) * p1)),((r * p1) * p2)) is Element of the U1 of CS

K4(((r * (r1 * p)) + ((r * p) * p1)),((r * p1) * p2)) is set

the U5 of CS . K4(((r * (r1 * p)) + ((r * p) * p1)),((r * p1) * p2)) is set

r * (p * p1) is Element of the U1 of CS

K138( the Mult of CS,r,(p * p1)) is set

K4(r,(p * p1)) is set

the Mult of CS . K4(r,(p * p1)) is set

(r * (r1 * p)) + (r * (p * p1)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r * (r1 * p)),(r * (p * p1))) is Element of the U1 of CS

K4((r * (r1 * p)),(r * (p * p1))) is set

the U5 of CS . K4((r * (r1 * p)),(r * (p * p1))) is set

((r * (r1 * p)) + (r * (p * p1))) + ((r * p1) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((r * (r1 * p)) + (r * (p * p1))),((r * p1) * p2)) is Element of the U1 of CS

K4(((r * (r1 * p)) + (r * (p * p1))),((r * p1) * p2)) is set

the U5 of CS . K4(((r * (r1 * p)) + (r * (p * p1))),((r * p1) * p2)) is set

r * ((r1 * p) + (p * p1)) is Element of the U1 of CS

K138( the Mult of CS,r,((r1 * p) + (p * p1))) is set

K4(r,((r1 * p) + (p * p1))) is set

the Mult of CS . K4(r,((r1 * p) + (p * p1))) is set

(r * ((r1 * p) + (p * p1))) + ((r * p1) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r * ((r1 * p) + (p * p1))),((r * p1) * p2)) is Element of the U1 of CS

K4((r * ((r1 * p) + (p * p1))),((r * p1) * p2)) is set

the U5 of CS . K4((r * ((r1 * p) + (p * p1))),((r * p1) * p2)) is set

r * (p1 * p2) is Element of the U1 of CS

K138( the Mult of CS,r,(p1 * p2)) is set

K4(r,(p1 * p2)) is set

the Mult of CS . K4(r,(p1 * p2)) is set

(r * ((r1 * p) + (p * p1))) + (r * (p1 * p2)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r * ((r1 * p) + (p * p1))),(r * (p1 * p2))) is Element of the U1 of CS

K4((r * ((r1 * p) + (p * p1))),(r * (p1 * p2))) is set

the U5 of CS . K4((r * ((r1 * p) + (p * p1))),(r * (p1 * p2))) is set

CS is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the U1 of CS is non empty set

p is Element of the U1 of CS

p1 is Element of the U1 of CS

p + p1 is Element of the U1 of CS

the U5 of CS is V7() V10(K33( the U1 of CS, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS))

K33( the U1 of CS, the U1 of CS) is non empty set

K33(K33( the U1 of CS, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS)) is non empty set

K142( the U1 of CS, the U5 of CS,p,p1) is Element of the U1 of CS

K4(p,p1) is set

the U5 of CS . K4(p,p1) is set

p2 is Element of the U1 of CS

(p + p1) + p2 is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p + p1),p2) is Element of the U1 of CS

K4((p + p1),p2) is set

the U5 of CS . K4((p + p1),p2) is set

r is Element of the U1 of CS

p + r is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,p,r) is Element of the U1 of CS

K4(p,r) is set

the U5 of CS . K4(p,r) is set

r1 is Element of the U1 of CS

r + r1 is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,r,r1) is Element of the U1 of CS

K4(r,r1) is set

the U5 of CS . K4(r,r1) is set

p1 + r1 is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,p1,r1) is Element of the U1 of CS

K4(p1,r1) is set

the U5 of CS . K4(p1,r1) is set

(p + r) + (p1 + r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p + r),(p1 + r1)) is Element of the U1 of CS

K4((p + r),(p1 + r1)) is set

the U5 of CS . K4((p + r),(p1 + r1)) is set

p is Element of the U1 of CS

(r + r1) + p is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r + r1),p) is Element of the U1 of CS

K4((r + r1),p) is set

the U5 of CS . K4((r + r1),p) is set

((p + p1) + p2) + ((r + r1) + p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((p + p1) + p2),((r + r1) + p)) is Element of the U1 of CS

K4(((p + p1) + p2),((r + r1) + p)) is set

the U5 of CS . K4(((p + p1) + p2),((r + r1) + p)) is set

p2 + p is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,p2,p) is Element of the U1 of CS

K4(p2,p) is set

the U5 of CS . K4(p2,p) is set

((p + r) + (p1 + r1)) + (p2 + p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((p + r) + (p1 + r1)),(p2 + p)) is Element of the U1 of CS

K4(((p + r) + (p1 + r1)),(p2 + p)) is set

the U5 of CS . K4(((p + r) + (p1 + r1)),(p2 + p)) is set

p + (p1 + r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,p,(p1 + r1)) is Element of the U1 of CS

K4(p,(p1 + r1)) is set

the U5 of CS . K4(p,(p1 + r1)) is set

r + (p + (p1 + r1)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,r,(p + (p1 + r1))) is Element of the U1 of CS

K4(r,(p + (p1 + r1))) is set

the U5 of CS . K4(r,(p + (p1 + r1))) is set

(r + (p + (p1 + r1))) + (p2 + p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r + (p + (p1 + r1))),(p2 + p)) is Element of the U1 of CS

K4((r + (p + (p1 + r1))),(p2 + p)) is set

the U5 of CS . K4((r + (p + (p1 + r1))),(p2 + p)) is set

(p + p1) + r1 is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p + p1),r1) is Element of the U1 of CS

K4((p + p1),r1) is set

the U5 of CS . K4((p + p1),r1) is set

r + ((p + p1) + r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,r,((p + p1) + r1)) is Element of the U1 of CS

K4(r,((p + p1) + r1)) is set

the U5 of CS . K4(r,((p + p1) + r1)) is set

(r + ((p + p1) + r1)) + (p2 + p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r + ((p + p1) + r1)),(p2 + p)) is Element of the U1 of CS

K4((r + ((p + p1) + r1)),(p2 + p)) is set

the U5 of CS . K4((r + ((p + p1) + r1)),(p2 + p)) is set

(r + r1) + (p + p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r + r1),(p + p1)) is Element of the U1 of CS

K4((r + r1),(p + p1)) is set

the U5 of CS . K4((r + r1),(p + p1)) is set

((r + r1) + (p + p1)) + (p2 + p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((r + r1) + (p + p1)),(p2 + p)) is Element of the U1 of CS

K4(((r + r1) + (p + p1)),(p2 + p)) is set

the U5 of CS . K4(((r + r1) + (p + p1)),(p2 + p)) is set

(p + p1) + (p2 + p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(p + p1),(p2 + p)) is Element of the U1 of CS

K4((p + p1),(p2 + p)) is set

the U5 of CS . K4((p + p1),(p2 + p)) is set

(r + r1) + ((p + p1) + (p2 + p)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r + r1),((p + p1) + (p2 + p))) is Element of the U1 of CS

K4((r + r1),((p + p1) + (p2 + p))) is set

the U5 of CS . K4((r + r1),((p + p1) + (p2 + p))) is set

((p + p1) + p2) + p is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((p + p1) + p2),p) is Element of the U1 of CS

K4(((p + p1) + p2),p) is set

the U5 of CS . K4(((p + p1) + p2),p) is set

(r + r1) + (((p + p1) + p2) + p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(r + r1),(((p + p1) + p2) + p)) is Element of the U1 of CS

K4((r + r1),(((p + p1) + p2) + p)) is set

the U5 of CS . K4((r + r1),(((p + p1) + p2) + p)) is set

CS is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the U1 of CS is non empty set

0. CS is zero Element of the U1 of CS

the U2 of CS is Element of the U1 of CS

p is Element of the U1 of CS

p1 is Element of the U1 of CS

p2 is Element of the U1 of CS

r is Element of the U1 of CS

r1 is Element of the U1 of CS

p is V24() V25() Element of REAL

p * p is Element of the U1 of CS

the Mult of CS is V7() V10(K33(REAL, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33(REAL, the U1 of CS), the U1 of CS))

K33(REAL, the U1 of CS) is non empty set

K33(K33(REAL, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33(REAL, the U1 of CS), the U1 of CS)) is non empty set

K138( the Mult of CS,p,p) is set

K4(p,p) is set

the Mult of CS . K4(p,p) is set

p1 is V24() V25() Element of REAL

p1 * p1 is Element of the U1 of CS

K138( the Mult of CS,p1,p1) is set

K4(p1,p1) is set

the Mult of CS . K4(p1,p1) is set

(p * p) + (p1 * p1) is Element of the U1 of CS

the U5 of CS is V7() V10(K33( the U1 of CS, the U1 of CS)) V11( the U1 of CS) Function-like quasi_total Element of K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS))

K33( the U1 of CS, the U1 of CS) is non empty set

K33(K33( the U1 of CS, the U1 of CS), the U1 of CS) is non empty set

K32(K33(K33( the U1 of CS, the U1 of CS), the U1 of CS)) is non empty set

K142( the U1 of CS, the U5 of CS,(p * p),(p1 * p1)) is Element of the U1 of CS

K4((p * p),(p1 * p1)) is set

the U5 of CS . K4((p * p),(p1 * p1)) is set

q is V24() V25() Element of REAL

q * p2 is Element of the U1 of CS

K138( the Mult of CS,q,p2) is set

K4(q,p2) is set

the Mult of CS . K4(q,p2) is set

((p * p) + (p1 * p1)) + (q * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((p * p) + (p1 * p1)),(q * p2)) is Element of the U1 of CS

K4(((p * p) + (p1 * p1)),(q * p2)) is set

the U5 of CS . K4(((p * p) + (p1 * p1)),(q * p2)) is set

q1 is V24() V25() Element of REAL

q1 * p is Element of the U1 of CS

K138( the Mult of CS,q1,p) is set

K4(q1,p) is set

the Mult of CS . K4(q1,p) is set

r is V24() V25() Element of REAL

r * p1 is Element of the U1 of CS

K138( the Mult of CS,r,p1) is set

K4(r,p1) is set

the Mult of CS . K4(r,p1) is set

(q1 * p) + (r * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(q1 * p),(r * p1)) is Element of the U1 of CS

K4((q1 * p),(r * p1)) is set

the U5 of CS . K4((q1 * p),(r * p1)) is set

y is V24() V25() Element of REAL

y * p2 is Element of the U1 of CS

K138( the Mult of CS,y,p2) is set

K4(y,p2) is set

the Mult of CS . K4(y,p2) is set

((q1 * p) + (r * p1)) + (y * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((q1 * p) + (r * p1)),(y * p2)) is Element of the U1 of CS

K4(((q1 * p) + (r * p1)),(y * p2)) is set

the U5 of CS . K4(((q1 * p) + (r * p1)),(y * p2)) is set

z2 is V24() V25() Element of REAL

z2 * r is Element of the U1 of CS

K138( the Mult of CS,z2,r) is set

K4(z2,r) is set

the Mult of CS . K4(z2,r) is set

z2 * p is V24() V25() Element of REAL

z2 * p1 is V24() V25() Element of REAL

z2 * q is V24() V25() Element of REAL

z1 is V24() V25() Element of REAL

z1 * r1 is Element of the U1 of CS

K138( the Mult of CS,z1,r1) is set

K4(z1,r1) is set

the Mult of CS . K4(z1,r1) is set

(z2 * r) + (z1 * r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(z2 * r),(z1 * r1)) is Element of the U1 of CS

K4((z2 * r),(z1 * r1)) is set

the U5 of CS . K4((z2 * r),(z1 * r1)) is set

z1 * q1 is V24() V25() Element of REAL

(z2 * p) + (z1 * q1) is V24() V25() Element of REAL

((z2 * p) + (z1 * q1)) * p is Element of the U1 of CS

K138( the Mult of CS,((z2 * p) + (z1 * q1)),p) is set

K4(((z2 * p) + (z1 * q1)),p) is set

the Mult of CS . K4(((z2 * p) + (z1 * q1)),p) is set

z1 * r is V24() V25() Element of REAL

(z2 * p1) + (z1 * r) is V24() V25() Element of REAL

((z2 * p1) + (z1 * r)) * p1 is Element of the U1 of CS

K138( the Mult of CS,((z2 * p1) + (z1 * r)),p1) is set

K4(((z2 * p1) + (z1 * r)),p1) is set

the Mult of CS . K4(((z2 * p1) + (z1 * r)),p1) is set

(((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((z2 * p) + (z1 * q1)) * p),(((z2 * p1) + (z1 * r)) * p1)) is Element of the U1 of CS

K4((((z2 * p) + (z1 * q1)) * p),(((z2 * p1) + (z1 * r)) * p1)) is set

the U5 of CS . K4((((z2 * p) + (z1 * q1)) * p),(((z2 * p1) + (z1 * r)) * p1)) is set

z1 * y is V24() V25() Element of REAL

(z2 * q) + (z1 * y) is V24() V25() Element of REAL

((z2 * q) + (z1 * y)) * p2 is Element of the U1 of CS

K138( the Mult of CS,((z2 * q) + (z1 * y)),p2) is set

K4(((z2 * q) + (z1 * y)),p2) is set

the Mult of CS . K4(((z2 * q) + (z1 * y)),p2) is set

((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)) + (((z2 * q) + (z1 * y)) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)),(((z2 * q) + (z1 * y)) * p2)) is Element of the U1 of CS

K4(((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)),(((z2 * q) + (z1 * y)) * p2)) is set

the U5 of CS . K4(((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)),(((z2 * q) + (z1 * y)) * p2)) is set

(z2 * p) * p is Element of the U1 of CS

K138( the Mult of CS,(z2 * p),p) is set

K4((z2 * p),p) is set

the Mult of CS . K4((z2 * p),p) is set

(z2 * p1) * p1 is Element of the U1 of CS

K138( the Mult of CS,(z2 * p1),p1) is set

K4((z2 * p1),p1) is set

the Mult of CS . K4((z2 * p1),p1) is set

((z2 * p) * p) + ((z2 * p1) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((z2 * p) * p),((z2 * p1) * p1)) is Element of the U1 of CS

K4(((z2 * p) * p),((z2 * p1) * p1)) is set

the U5 of CS . K4(((z2 * p) * p),((z2 * p1) * p1)) is set

(z2 * q) * p2 is Element of the U1 of CS

K138( the Mult of CS,(z2 * q),p2) is set

K4((z2 * q),p2) is set

the Mult of CS . K4((z2 * q),p2) is set

(((z2 * p) * p) + ((z2 * p1) * p1)) + ((z2 * q) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((z2 * p) * p) + ((z2 * p1) * p1)),((z2 * q) * p2)) is Element of the U1 of CS

K4((((z2 * p) * p) + ((z2 * p1) * p1)),((z2 * q) * p2)) is set

the U5 of CS . K4((((z2 * p) * p) + ((z2 * p1) * p1)),((z2 * q) * p2)) is set

(z1 * q1) * p is Element of the U1 of CS

K138( the Mult of CS,(z1 * q1),p) is set

K4((z1 * q1),p) is set

the Mult of CS . K4((z1 * q1),p) is set

(z1 * r) * p1 is Element of the U1 of CS

K138( the Mult of CS,(z1 * r),p1) is set

K4((z1 * r),p1) is set

the Mult of CS . K4((z1 * r),p1) is set

((z1 * q1) * p) + ((z1 * r) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((z1 * q1) * p),((z1 * r) * p1)) is Element of the U1 of CS

K4(((z1 * q1) * p),((z1 * r) * p1)) is set

the U5 of CS . K4(((z1 * q1) * p),((z1 * r) * p1)) is set

(z1 * y) * p2 is Element of the U1 of CS

K138( the Mult of CS,(z1 * y),p2) is set

K4((z1 * y),p2) is set

the Mult of CS . K4((z1 * y),p2) is set

(((z1 * q1) * p) + ((z1 * r) * p1)) + ((z1 * y) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((z1 * q1) * p) + ((z1 * r) * p1)),((z1 * y) * p2)) is Element of the U1 of CS

K4((((z1 * q1) * p) + ((z1 * r) * p1)),((z1 * y) * p2)) is set

the U5 of CS . K4((((z1 * q1) * p) + ((z1 * r) * p1)),((z1 * y) * p2)) is set

((((z2 * p) * p) + ((z2 * p1) * p1)) + ((z2 * q) * p2)) + ((((z1 * q1) * p) + ((z1 * r) * p1)) + ((z1 * y) * p2)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((z2 * p) * p) + ((z2 * p1) * p1)) + ((z2 * q) * p2)),((((z1 * q1) * p) + ((z1 * r) * p1)) + ((z1 * y) * p2))) is Element of the U1 of CS

K4(((((z2 * p) * p) + ((z2 * p1) * p1)) + ((z2 * q) * p2)),((((z1 * q1) * p) + ((z1 * r) * p1)) + ((z1 * y) * p2))) is set

the U5 of CS . K4(((((z2 * p) * p) + ((z2 * p1) * p1)) + ((z2 * q) * p2)),((((z1 * q1) * p) + ((z1 * r) * p1)) + ((z1 * y) * p2))) is set

((z2 * p) * p) + ((z1 * q1) * p) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((z2 * p) * p),((z1 * q1) * p)) is Element of the U1 of CS

K4(((z2 * p) * p),((z1 * q1) * p)) is set

the U5 of CS . K4(((z2 * p) * p),((z1 * q1) * p)) is set

((z2 * p1) * p1) + ((z1 * r) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((z2 * p1) * p1),((z1 * r) * p1)) is Element of the U1 of CS

K4(((z2 * p1) * p1),((z1 * r) * p1)) is set

the U5 of CS . K4(((z2 * p1) * p1),((z1 * r) * p1)) is set

(((z2 * p) * p) + ((z1 * q1) * p)) + (((z2 * p1) * p1) + ((z1 * r) * p1)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((z2 * p) * p) + ((z1 * q1) * p)),(((z2 * p1) * p1) + ((z1 * r) * p1))) is Element of the U1 of CS

K4((((z2 * p) * p) + ((z1 * q1) * p)),(((z2 * p1) * p1) + ((z1 * r) * p1))) is set

the U5 of CS . K4((((z2 * p) * p) + ((z1 * q1) * p)),(((z2 * p1) * p1) + ((z1 * r) * p1))) is set

((z2 * q) * p2) + ((z1 * y) * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((z2 * q) * p2),((z1 * y) * p2)) is Element of the U1 of CS

K4(((z2 * q) * p2),((z1 * y) * p2)) is set

the U5 of CS . K4(((z2 * q) * p2),((z1 * y) * p2)) is set

((((z2 * p) * p) + ((z1 * q1) * p)) + (((z2 * p1) * p1) + ((z1 * r) * p1))) + (((z2 * q) * p2) + ((z1 * y) * p2)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((z2 * p) * p) + ((z1 * q1) * p)) + (((z2 * p1) * p1) + ((z1 * r) * p1))),(((z2 * q) * p2) + ((z1 * y) * p2))) is Element of the U1 of CS

K4(((((z2 * p) * p) + ((z1 * q1) * p)) + (((z2 * p1) * p1) + ((z1 * r) * p1))),(((z2 * q) * p2) + ((z1 * y) * p2))) is set

the U5 of CS . K4(((((z2 * p) * p) + ((z1 * q1) * p)) + (((z2 * p1) * p1) + ((z1 * r) * p1))),(((z2 * q) * p2) + ((z1 * y) * p2))) is set

(((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) * p1) + ((z1 * r) * p1)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((z2 * p) + (z1 * q1)) * p),(((z2 * p1) * p1) + ((z1 * r) * p1))) is Element of the U1 of CS

K4((((z2 * p) + (z1 * q1)) * p),(((z2 * p1) * p1) + ((z1 * r) * p1))) is set

the U5 of CS . K4((((z2 * p) + (z1 * q1)) * p),(((z2 * p1) * p1) + ((z1 * r) * p1))) is set

((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) * p1) + ((z1 * r) * p1))) + (((z2 * q) * p2) + ((z1 * y) * p2)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) * p1) + ((z1 * r) * p1))),(((z2 * q) * p2) + ((z1 * y) * p2))) is Element of the U1 of CS

K4(((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) * p1) + ((z1 * r) * p1))),(((z2 * q) * p2) + ((z1 * y) * p2))) is set

the U5 of CS . K4(((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) * p1) + ((z1 * r) * p1))),(((z2 * q) * p2) + ((z1 * y) * p2))) is set

((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)) + (((z2 * q) * p2) + ((z1 * y) * p2)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)),(((z2 * q) * p2) + ((z1 * y) * p2))) is Element of the U1 of CS

K4(((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)),(((z2 * q) * p2) + ((z1 * y) * p2))) is set

the U5 of CS . K4(((((z2 * p) + (z1 * q1)) * p) + (((z2 * p1) + (z1 * r)) * p1)),(((z2 * q) * p2) + ((z1 * y) * p2))) is set

z2 is Element of the U1 of CS

z1 is Element of the U1 of CS

x2 is Element of the U1 of CS

y " is V24() V25() Element of REAL

q * (y ") is V24() V25() Element of REAL

- (q * (y ")) is V24() V25() Element of REAL

1 * r is Element of the U1 of CS

K138( the Mult of CS,1,r) is set

K4(1,r) is set

the Mult of CS . K4(1,r) is set

(- (q * (y "))) * r1 is Element of the U1 of CS

K138( the Mult of CS,(- (q * (y "))),r1) is set

K4((- (q * (y "))),r1) is set

the Mult of CS . K4((- (q * (y "))),r1) is set

(1 * r) + ((- (q * (y "))) * r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * r),((- (q * (y "))) * r1)) is Element of the U1 of CS

K4((1 * r),((- (q * (y "))) * r1)) is set

the U5 of CS . K4((1 * r),((- (q * (y "))) * r1)) is set

- r1 is Element of the U1 of CS

(q * (y ")) * (- r1) is Element of the U1 of CS

K138( the Mult of CS,(q * (y ")),(- r1)) is set

K4((q * (y ")),(- r1)) is set

the Mult of CS . K4((q * (y ")),(- r1)) is set

(1 * r) + ((q * (y ")) * (- r1)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * r),((q * (y ")) * (- r1))) is Element of the U1 of CS

K4((1 * r),((q * (y ")) * (- r1))) is set

the U5 of CS . K4((1 * r),((q * (y ")) * (- r1))) is set

(q * (y ")) * r1 is Element of the U1 of CS

K138( the Mult of CS,(q * (y ")),r1) is set

K4((q * (y ")),r1) is set

the Mult of CS . K4((q * (y ")),r1) is set

- ((q * (y ")) * r1) is Element of the U1 of CS

(1 * r) + (- ((q * (y ")) * r1)) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * r),(- ((q * (y ")) * r1))) is Element of the U1 of CS

K4((1 * r),(- ((q * (y ")) * r1))) is set

the U5 of CS . K4((1 * r),(- ((q * (y ")) * r1))) is set

- (1 * r) is Element of the U1 of CS

1 * q is V24() V25() Element of REAL

(- (q * (y "))) * y is V24() V25() Element of REAL

(1 * q) + ((- (q * (y "))) * y) is V24() V25() Element of REAL

- q is V24() V25() Element of REAL

(y ") * y is V24() V25() Element of REAL

(- q) * ((y ") * y) is V24() V25() Element of REAL

q + ((- q) * ((y ") * y)) is V24() V25() Element of REAL

(- q) * 1 is V24() V25() Element of REAL

q + ((- q) * 1) is V24() V25() Element of REAL

1 * p is V24() V25() Element of REAL

(- (q * (y "))) * q1 is V24() V25() Element of REAL

(1 * p) + ((- (q * (y "))) * q1) is V24() V25() Element of REAL

((1 * p) + ((- (q * (y "))) * q1)) * p is Element of the U1 of CS

K138( the Mult of CS,((1 * p) + ((- (q * (y "))) * q1)),p) is set

K4(((1 * p) + ((- (q * (y "))) * q1)),p) is set

the Mult of CS . K4(((1 * p) + ((- (q * (y "))) * q1)),p) is set

1 * p1 is V24() V25() Element of REAL

(- (q * (y "))) * r is V24() V25() Element of REAL

(1 * p1) + ((- (q * (y "))) * r) is V24() V25() Element of REAL

((1 * p1) + ((- (q * (y "))) * r)) * p1 is Element of the U1 of CS

K138( the Mult of CS,((1 * p1) + ((- (q * (y "))) * r)),p1) is set

K4(((1 * p1) + ((- (q * (y "))) * r)),p1) is set

the Mult of CS . K4(((1 * p1) + ((- (q * (y "))) * r)),p1) is set

(((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((1 * p) + ((- (q * (y "))) * q1)) * p),(((1 * p1) + ((- (q * (y "))) * r)) * p1)) is Element of the U1 of CS

K4((((1 * p) + ((- (q * (y "))) * q1)) * p),(((1 * p1) + ((- (q * (y "))) * r)) * p1)) is set

the U5 of CS . K4((((1 * p) + ((- (q * (y "))) * q1)) * p),(((1 * p1) + ((- (q * (y "))) * r)) * p1)) is set

0 * p2 is Element of the U1 of CS

K138( the Mult of CS,0,p2) is set

K4(0,p2) is set

the Mult of CS . K4(0,p2) is set

((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)) + (0 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)),(0 * p2)) is Element of the U1 of CS

K4(((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)),(0 * p2)) is set

the U5 of CS . K4(((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)),(0 * p2)) is set

((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)),(0. CS)) is Element of the U1 of CS

K4(((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)),(0. CS)) is set

the U5 of CS . K4(((((1 * p) + ((- (q * (y "))) * q1)) * p) + (((1 * p1) + ((- (q * (y "))) * r)) * p1)),(0. CS)) is set

0 * r is Element of the U1 of CS

K138( the Mult of CS,0,r) is set

K4(0,r) is set

the Mult of CS . K4(0,r) is set

1 * r1 is Element of the U1 of CS

K138( the Mult of CS,1,r1) is set

K4(1,r1) is set

the Mult of CS . K4(1,r1) is set

(0 * r) + (1 * r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0 * r),(1 * r1)) is Element of the U1 of CS

K4((0 * r),(1 * r1)) is set

the U5 of CS . K4((0 * r),(1 * r1)) is set

(0 * r) + r1 is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0 * r),r1) is Element of the U1 of CS

K4((0 * r),r1) is set

the U5 of CS . K4((0 * r),r1) is set

(0. CS) + r1 is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(0. CS),r1) is Element of the U1 of CS

K4((0. CS),r1) is set

the U5 of CS . K4((0. CS),r1) is set

0 * q is V24() V25() Element of REAL

1 * y is V24() V25() Element of REAL

(0 * q) + (1 * y) is V24() V25() Element of REAL

0 * p is V24() V25() Element of REAL

1 * q1 is V24() V25() Element of REAL

(0 * p) + (1 * q1) is V24() V25() Element of REAL

((0 * p) + (1 * q1)) * p is Element of the U1 of CS

K138( the Mult of CS,((0 * p) + (1 * q1)),p) is set

K4(((0 * p) + (1 * q1)),p) is set

the Mult of CS . K4(((0 * p) + (1 * q1)),p) is set

0 * p1 is V24() V25() Element of REAL

1 * r is V24() V25() Element of REAL

(0 * p1) + (1 * r) is V24() V25() Element of REAL

((0 * p1) + (1 * r)) * p1 is Element of the U1 of CS

K138( the Mult of CS,((0 * p1) + (1 * r)),p1) is set

K4(((0 * p1) + (1 * r)),p1) is set

the Mult of CS . K4(((0 * p1) + (1 * r)),p1) is set

(((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((0 * p) + (1 * q1)) * p),(((0 * p1) + (1 * r)) * p1)) is Element of the U1 of CS

K4((((0 * p) + (1 * q1)) * p),(((0 * p1) + (1 * r)) * p1)) is set

the U5 of CS . K4((((0 * p) + (1 * q1)) * p),(((0 * p1) + (1 * r)) * p1)) is set

((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)) + (0 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)),(0 * p2)) is Element of the U1 of CS

K4(((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)),(0 * p2)) is set

the U5 of CS . K4(((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)),(0 * p2)) is set

((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)),(0. CS)) is Element of the U1 of CS

K4(((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)),(0. CS)) is set

the U5 of CS . K4(((((0 * p) + (1 * q1)) * p) + (((0 * p1) + (1 * r)) * p1)),(0. CS)) is set

z2 is Element of the U1 of CS

z1 is Element of the U1 of CS

0 * r1 is Element of the U1 of CS

K138( the Mult of CS,0,r1) is set

K4(0,r1) is set

the Mult of CS . K4(0,r1) is set

(1 * r) + (0 * r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(1 * r),(0 * r1)) is Element of the U1 of CS

K4((1 * r),(0 * r1)) is set

the U5 of CS . K4((1 * r),(0 * r1)) is set

r + (0 * r1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,r,(0 * r1)) is Element of the U1 of CS

K4(r,(0 * r1)) is set

the U5 of CS . K4(r,(0 * r1)) is set

r + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,r,(0. CS)) is Element of the U1 of CS

K4(r,(0. CS)) is set

the U5 of CS . K4(r,(0. CS)) is set

0 * y is V24() V25() Element of REAL

(1 * q) + (0 * y) is V24() V25() Element of REAL

0 * q1 is V24() V25() Element of REAL

(1 * p) + (0 * q1) is V24() V25() Element of REAL

((1 * p) + (0 * q1)) * p is Element of the U1 of CS

K138( the Mult of CS,((1 * p) + (0 * q1)),p) is set

K4(((1 * p) + (0 * q1)),p) is set

the Mult of CS . K4(((1 * p) + (0 * q1)),p) is set

0 * r is V24() V25() Element of REAL

(1 * p1) + (0 * r) is V24() V25() Element of REAL

((1 * p1) + (0 * r)) * p1 is Element of the U1 of CS

K138( the Mult of CS,((1 * p1) + (0 * r)),p1) is set

K4(((1 * p1) + (0 * r)),p1) is set

the Mult of CS . K4(((1 * p1) + (0 * r)),p1) is set

(((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,(((1 * p) + (0 * q1)) * p),(((1 * p1) + (0 * r)) * p1)) is Element of the U1 of CS

K4((((1 * p) + (0 * q1)) * p),(((1 * p1) + (0 * r)) * p1)) is set

the U5 of CS . K4((((1 * p) + (0 * q1)) * p),(((1 * p1) + (0 * r)) * p1)) is set

((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)) + (0 * p2) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)),(0 * p2)) is Element of the U1 of CS

K4(((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)),(0 * p2)) is set

the U5 of CS . K4(((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)),(0 * p2)) is set

((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)) + (0. CS) is Element of the U1 of CS

K142( the U1 of CS, the U5 of CS,((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)),(0. CS)) is Element of the U1 of CS

K4(((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)),(0. CS)) is set

the U5 of CS . K4(((((1 * p) + (0 * q1)) * p) + (((1 * p1) + (0 * r)) * p1)),(0. CS)) is set

z2 is Element of the U1 of CS

z2 is Element of the U1 of CS

z1 is Element of the U1 of CS

x2 is Element of the U1 of CS

CS is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the U1 of CS is non empty set

p is Element of the U1 of CS

p1 is Element of the U1 of CS

p2 is Element of the U1 of CS

r is Element of the