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