:: MATRIX14 semantic presentation

REAL is set

NAT is non empty V21() V22() V23() V28() V33() V34() Element of bool REAL

bool REAL is set

{} is set

the Relation-like non-empty empty-yielding functional empty V21() V22() V23() V25() V26() V27() V28() V33() V35( {} ) FinSequence-like FinSequence-membered V47() V48() ext-real non positive non negative set is Relation-like non-empty empty-yielding functional empty V21() V22() V23() V25() V26() V27() V28() V33() V35( {} ) FinSequence-like FinSequence-membered V47() V48() ext-real non positive non negative set

1 is non empty V21() V22() V23() V27() V28() V33() V47() V48() ext-real positive non negative Element of NAT

{{},1} is set

NAT is non empty V21() V22() V23() V28() V33() V34() set

bool NAT is V28() set

bool NAT is V28() set

K183(NAT) is V45() set

COMPLEX is set

RAT is set

INT is set

[:1,1:] is Relation-like set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like set

bool [:[:1,1:],1:] is set

[:[:1,1:],REAL:] is Relation-like set

bool [:[:1,1:],REAL:] is set

[:REAL,REAL:] is Relation-like set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is set

2 is non empty V21() V22() V23() V27() V28() V33() V47() V48() ext-real positive non negative Element of NAT

[:2,2:] is Relation-like set

[:[:2,2:],REAL:] is Relation-like set

bool [:[:2,2:],REAL:] is set

bool [:REAL,REAL:] is set

K386(2) is V166() L15()

the carrier of K386(2) is set

0 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

3 is non empty V21() V22() V23() V27() V28() V33() V47() V48() ext-real positive non negative Element of NAT

Seg 1 is non empty trivial V28() V35(1) Element of bool NAT

{1} is non empty trivial V35(1) set

Seg 2 is non empty V28() V35(2) Element of bool NAT

{1,2} is set

n is non empty ZeroStr

the carrier of n is non empty set

K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

0. n is V83(n) Element of the carrier of n

K |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of n

K -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

n is non empty ZeroStr

K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(n,K) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

the carrier of n is non empty set

0. n is V83(n) Element of the carrier of n

K |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of n

K -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

n is non empty addLoopStr

the carrier of n is non empty set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

{ b

n is non empty addLoopStr

the carrier of n is non empty set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K + A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len (K + A) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B2 + B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

dom (B2 + B3) is V35( len K) Element of bool NAT

Seg (len K) is V28() V35( len K) Element of bool NAT

n is non empty addLoopStr

the carrier of n is non empty set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K - A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len (K - A) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B2 - B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

dom (B2 - B3) is V35( len K) Element of bool NAT

Seg (len K) is V28() V35( len K) Element of bool NAT

n is non empty multLoopStr

the carrier of n is non empty set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

mlt (K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

dom (mlt (K,A)) is Element of bool NAT

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(mlt (K,A)) . B is set

K /. B is Element of the carrier of n

A /. B is Element of the carrier of n

(K /. B) * (A /. B) is Element of the carrier of n

the multF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the multF of n . ((K /. B),(A /. B)) is Element of the carrier of n

(mlt (K,A)) /. B is Element of the carrier of n

the multF of n .: (K,A) is Relation-like Function-like set

rng A is set

dom the multF of n is set

rng K is set

[:(rng K),(rng A):] is Relation-like set

dom K is Element of bool NAT

dom A is Element of bool NAT

(dom K) /\ (dom A) is Element of bool NAT

A . B is set

K . B is set

n is non empty addLoopStr

the carrier of n is non empty set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K + A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K - A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

(K + A) . B is set

K /. B is Element of the carrier of n

A /. B is Element of the carrier of n

(K /. B) + (A /. B) is Element of the carrier of n

the addF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the addF of n . ((K /. B),(A /. B)) is Element of the carrier of n

(K - A) . B is set

(K /. B) - (A /. B) is Element of the carrier of n

- (A /. B) is Element of the carrier of n

(K /. B) + (- (A /. B)) is Element of the carrier of n

the addF of n . ((K /. B),(- (A /. B))) is Element of the carrier of n

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B2 /. B is Element of the carrier of n

B2 . B is set

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B3 /. B is Element of the carrier of n

B3 . B is set

Seg (len K) is V28() V35( len K) Element of bool NAT

len (K + A) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (len (K + A)) is V28() V35( len (K + A)) Element of bool NAT

dom (K + A) is Element of bool NAT

len (K - A) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (len (K - A)) is V28() V35( len (K - A)) Element of bool NAT

dom (K - A) is Element of bool NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is Element of the carrier of n

- K is Element of the carrier of n

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K * A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

- (K * A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(- K) * A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

- A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K * (- A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(len A) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

K * B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

1_ n is Element of the carrier of n

1. n is V83(n) Element of the carrier of n

- (1_ n) is Element of the carrier of n

(- (1_ n)) * B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

(- (1_ n)) * K is Element of the carrier of n

the multF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the multF of n . ((- (1_ n)),K) is Element of the carrier of n

((- (1_ n)) * K) * B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

(1_ n) * K is Element of the carrier of n

the multF of n . ((1_ n),K) is Element of the carrier of n

- ((1_ n) * K) is Element of the carrier of n

(- ((1_ n) * K)) * B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

(- (1_ n)) * B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

K * ((- (1_ n)) * B2) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

n is non empty multLoopStr

the carrier of n is non empty set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K ^ B is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

A ^ B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

mlt ((K ^ B),(A ^ B2)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

mlt (K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

mlt (B,B2) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(mlt (K,A)) ^ (mlt (B,B2)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

the multF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the multF of n .: ((K ^ B),(A ^ B2)) is Relation-like Function-like set

<:(K ^ B),(A ^ B2):> is Relation-like Function-like set

<:(K ^ B),(A ^ B2):> * the multF of n is Relation-like set

dom (K ^ B) is Element of bool NAT

len (K ^ B) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (len (K ^ B)) is V28() V35( len (K ^ B)) Element of bool NAT

rng (A ^ B2) is set

dom the multF of n is set

rng (K ^ B) is set

[:(rng (K ^ B)),(rng (A ^ B2)):] is Relation-like set

dom (<:(K ^ B),(A ^ B2):> * the multF of n) is set

dom (A ^ B2) is Element of bool NAT

(dom (K ^ B)) /\ (dom (A ^ B2)) is Element of bool NAT

len (A ^ B2) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(len A) + (len B2) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (len (A ^ B2)) is V28() V35( len (A ^ B2)) Element of bool NAT

dom (mlt ((K ^ B),(A ^ B2))) is Element of bool NAT

the multF of n .: (B,B2) is Relation-like Function-like set

<:B,B2:> is Relation-like Function-like set

<:B,B2:> * the multF of n is Relation-like set

rng B is set

rng B2 is set

[:(rng B),(rng B2):] is Relation-like set

dom (<:B,B2:> * the multF of n) is set

dom B is Element of bool NAT

dom B2 is Element of bool NAT

(dom B) /\ (dom B2) is Element of bool NAT

Seg (len B) is V28() V35( len B) Element of bool NAT

dom (mlt (B,B2)) is Element of bool NAT

len (mlt (B,B2)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

the multF of n .: (K,A) is Relation-like Function-like set

<:K,A:> is Relation-like Function-like set

<:K,A:> * the multF of n is Relation-like set

rng K is set

rng A is set

[:(rng K),(rng A):] is Relation-like set

dom (<:K,A:> * the multF of n) is set

dom K is Element of bool NAT

dom A is Element of bool NAT

(dom K) /\ (dom A) is Element of bool NAT

(len K) + (len B) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (len K) is V28() V35( len K) Element of bool NAT

dom (mlt (K,A)) is Element of bool NAT

len (mlt ((K ^ B),(A ^ B2))) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B3 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

(mlt ((K ^ B),(A ^ B2))) . B3 is set

((mlt (K,A)) ^ (mlt (B,B2))) . B3 is set

Seg (len (mlt ((K ^ B),(A ^ B2)))) is V28() V35( len (mlt ((K ^ B),(A ^ B2)))) Element of bool NAT

(K ^ B) /. B3 is Element of the carrier of n

(K ^ B) . B3 is set

(A ^ B2) /. B3 is Element of the carrier of n

(A ^ B2) . B3 is set

A . B3 is set

(mlt (K,A)) . B3 is set

K /. B3 is Element of the carrier of n

A /. B3 is Element of the carrier of n

(K /. B3) * (A /. B3) is Element of the carrier of n

the multF of n . ((K /. B3),(A /. B3)) is Element of the carrier of n

K . B3 is set

((K ^ B) /. B3) * ((A ^ B2) /. B3) is Element of the carrier of n

the multF of n . (((K ^ B) /. B3),((A ^ B2) /. B3)) is Element of the carrier of n

B3 -' (len K) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B3 - (len K) is V47() V48() ext-real set

(len K) + (B3 -' (len K)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

((len K) + (len B)) - (len K) is V47() V48() ext-real set

0 + 1 is non empty V21() V22() V23() V27() V28() V33() V47() V48() ext-real positive non negative Element of NAT

len (mlt (K,A)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(len (mlt (K,A))) + (B3 -' (len K)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(mlt (B,B2)) . (B3 -' (len K)) is set

B /. (B3 -' (len K)) is Element of the carrier of n

B2 /. (B3 -' (len K)) is Element of the carrier of n

(B /. (B3 -' (len K))) * (B2 /. (B3 -' (len K))) is Element of the carrier of n

the multF of n . ((B /. (B3 -' (len K))),(B2 /. (B3 -' (len K)))) is Element of the carrier of n

B . (B3 -' (len K)) is set

B2 . (B3 -' (len K)) is set

((K ^ B) /. B3) * ((A ^ B2) /. B3) is Element of the carrier of n

the multF of n . (((K ^ B) /. B3),((A ^ B2) /. B3)) is Element of the carrier of n

((K ^ B) /. B3) * ((A ^ B2) /. B3) is Element of the carrier of n

the multF of n . (((K ^ B) /. B3),((A ^ B2) /. B3)) is Element of the carrier of n

((K ^ B) /. B3) * ((A ^ B2) /. B3) is Element of the carrier of n

the multF of n . (((K ^ B) /. B3),((A ^ B2) /. B3)) is Element of the carrier of n

len (mlt (K,A)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(len (mlt (K,A))) + (len (mlt (B,B2))) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

len ((mlt (K,A)) ^ (mlt (B,B2))) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

mlt (K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B is Element of the carrier of n

B * K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

mlt ((B * K),A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B * (mlt (K,A)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B * A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

mlt (K,(B * A)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

mlt (B3,B2) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B * (mlt (B3,B2)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K "*" A is Element of the carrier of n

B is Element of the carrier of n

B * K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(B * K) "*" A is Element of the carrier of n

B * (K "*" A) is Element of the carrier of n

the multF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the multF of n . (B,(K "*" A)) is Element of the carrier of n

mlt ((B * K),A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (mlt ((B * K),A)) is Element of the carrier of n

mlt (K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B * (mlt (K,A)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (B * (mlt (K,A))) is Element of the carrier of n

Sum (mlt (K,A)) is Element of the carrier of n

B * (Sum (mlt (K,A))) is Element of the carrier of n

the multF of n . (B,(Sum (mlt (K,A)))) is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K "*" A is Element of the carrier of n

B is Element of the carrier of n

B * A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K "*" (B * A) is Element of the carrier of n

B * (K "*" A) is Element of the carrier of n

the multF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the multF of n . (B,(K "*" A)) is Element of the carrier of n

mlt (K,(B * A)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (mlt (K,(B * A))) is Element of the carrier of n

mlt (K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B * (mlt (K,A)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (B * (mlt (K,A))) is Element of the carrier of n

Sum (mlt (K,A)) is Element of the carrier of n

B * (Sum (mlt (K,A))) is Element of the carrier of n

the multF of n . (B,(Sum (mlt (K,A)))) is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A + B is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K "*" (A + B) is Element of the carrier of n

K "*" A is Element of the carrier of n

K "*" B is Element of the carrier of n

(K "*" A) + (K "*" B) is Element of the carrier of n

the addF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the addF of n . ((K "*" A),(K "*" B)) is Element of the carrier of n

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

mlt (K,(A + B)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (mlt (K,(A + B))) is Element of the carrier of n

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

mlt (B3,B2) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

B is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

mlt (B3,B) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

(mlt (B3,B2)) + (mlt (B3,B)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

Sum ((mlt (B3,B2)) + (mlt (B3,B))) is Element of the carrier of n

Sum (mlt (B3,B2)) is Element of the carrier of n

Sum (mlt (B3,B)) is Element of the carrier of n

(Sum (mlt (B3,B2))) + (Sum (mlt (B3,B))) is Element of the carrier of n

the addF of n . ((Sum (mlt (B3,B2))),(Sum (mlt (B3,B)))) is Element of the carrier of n

mlt (K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (mlt (K,A)) is Element of the carrier of n

(Sum (mlt (K,A))) + (K "*" B) is Element of the carrier of n

the addF of n . ((Sum (mlt (K,A))),(K "*" B)) is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K ^ B is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

A ^ B2 is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(K ^ B) "*" (A ^ B2) is Element of the carrier of n

K "*" A is Element of the carrier of n

B "*" B2 is Element of the carrier of n

(K "*" A) + (B "*" B2) is Element of the carrier of n

the addF of n is Relation-like Function-like V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

the addF of n . ((K "*" A),(B "*" B2)) is Element of the carrier of n

mlt (K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

mlt (B,B2) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(mlt (K,A)) ^ (mlt (B,B2)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum ((mlt (K,A)) ^ (mlt (B,B2))) is Element of the carrier of n

Sum (mlt (K,A)) is Element of the carrier of n

Sum (mlt (B,B2)) is Element of the carrier of n

(Sum (mlt (K,A))) + (Sum (mlt (B,B2))) is Element of the carrier of n

the addF of n . ((Sum (mlt (K,A))),(Sum (mlt (B,B2)))) is Element of the carrier of n

mlt ((K ^ B),(A ^ B2)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (mlt ((K ^ B),(A ^ B2))) is Element of the carrier of n

(Sum (mlt (K,A))) + (B "*" B2) is Element of the carrier of n

the addF of n . ((Sum (mlt (K,A))),(B "*" B2)) is Element of the carrier of n

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

n -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

0. K is V83(K) Element of the carrier of K

n |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

A is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

mlt (A,(n |-> (0. K))) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

(K,n) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

(0. K) * (K,n) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

mlt (A,((0. K) * (K,n))) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

mlt (A,(K,n)) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

(0. K) * (mlt (A,(K,n))) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

1. (n,0) is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

the carrier of n is non empty non trivial set

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

0. (n,0) is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

0 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

0. n is V83(n) Element of the carrier of n

0 |-> (0. n) is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like functional empty V21() V22() V23() V25() V26() V27() V28() V33() V35( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V40() V47() V48() ext-real non positive non negative Element of 0 -tuples_on the carrier of n

0 |-> (0 |-> (0. n)) is Relation-like non-empty empty-yielding NAT -defined 0 -tuples_on the carrier of n -valued Function-like functional empty V21() V22() V23() V25() V26() V27() V28() V33() V35( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V40() V47() V48() ext-real non positive non negative Element of 0 -tuples_on (0 -tuples_on the carrier of n)

0 -tuples_on (0 -tuples_on the carrier of n) is functional non empty FinSequence-membered FinSequenceSet of 0 -tuples_on the carrier of n

len (1. (n,0)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

1. (n,0) is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

0. (n,0) is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

0 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

0. n is V83(n) Element of the carrier of n

0 |-> (0. n) is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued Function-like functional empty V21() V22() V23() V25() V26() V27() V28() V33() V35( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V40() V47() V48() ext-real non positive non negative Element of 0 -tuples_on the carrier of n

0 |-> (0 |-> (0. n)) is Relation-like non-empty empty-yielding NAT -defined 0 -tuples_on the carrier of n -valued Function-like functional empty V21() V22() V23() V25() V26() V27() V28() V33() V35( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V40() V47() V48() ext-real non positive non negative Element of 0 -tuples_on (0 -tuples_on the carrier of n)

0 -tuples_on (0 -tuples_on the carrier of n) is functional non empty FinSequence-membered FinSequenceSet of 0 -tuples_on the carrier of n

K is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

K is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

K * K is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

1. (n,0) is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of 0 , 0 , the carrier of n

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A * B is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B2 is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

(A * B) * B2 is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B * B2 is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A * (B * B2) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

width B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

len B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

width A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

len B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A ~ is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B * A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A * B is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A ~ is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

(A ~) * A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A * (A ~) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B * A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

A * B is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

0. n is V83(n) Element of the carrier of n

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(n,(len K)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

(len K) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

K "*" (n,(len K)) is Element of the carrier of n

B is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

mlt (B,(n,(len K))) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

Sum (mlt (B,(n,(len K)))) is Element of the carrier of n

Sum (n,(len K)) is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

0. n is V83(n) Element of the carrier of n

K is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(n,(len K)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

(len K) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35( len K) FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

(n,(len K)) "*" K is Element of the carrier of n

K "*" (n,(len K)) is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

0. n is V83(n) Element of the carrier of n

<*(0. n)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty trivial V28() V35(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K is Element of the carrier of n

<*K*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty trivial V28() V35(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*(0. n)*> "*" <*K*> is Element of the carrier of n

len <*K*> is non empty V21() V22() V23() V27() V28() V33() V47() V48() ext-real positive non negative Element of NAT

(n,1) is Relation-like NAT -defined the carrier of n -valued Function-like non empty trivial V28() V35(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n

1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

1 |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like non empty trivial V28() V35(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n

(n,1) "*" <*K*> is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

0. n is V83(n) Element of the carrier of n

K |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of n

K -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

1. n is V83(n) Element of the carrier of n

Replace ((K |-> (0. n)),A,(1. n)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

(n,K,A) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

the carrier of n is non empty non trivial set

0. n is V83(n) Element of the carrier of n

K |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of n

K -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

1. n is V83(n) Element of the carrier of n

Replace ((K |-> (0. n)),A,(1. n)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len (n,K,A) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

len (Replace ((K |-> (0. n)),A,(1. n))) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

len (K |-> (0. n)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

1. n is V83(n) Element of the carrier of n

the carrier of n is non empty non trivial set

K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

(n,A,K) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

0. n is V83(n) Element of the carrier of n

A |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35(A) FinSequence-like FinSubsequence-like Element of A -tuples_on the carrier of n

A -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

Replace ((A |-> (0. n)),K,(1. n)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(n,A,K) . K is set

len (A |-> (0. n)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

len (Replace ((A |-> (0. n)),K,(1. n))) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(Replace ((A |-> (0. n)),K,(1. n))) /. K is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

0. n is V83(n) Element of the carrier of n

the carrier of n is non empty non trivial set

A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

(n,B,K) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35(B) FinSequence-like FinSubsequence-like Element of B -tuples_on the carrier of n

B -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

1. n is V83(n) Element of the carrier of n

Replace ((B |-> (0. n)),K,(1. n)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(n,B,K) . A is set

Seg B is V28() V35(B) Element of bool NAT

len (B |-> (0. n)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

len (Replace ((B |-> (0. n)),K,(1. n))) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(Replace ((B |-> (0. n)),K,(1. n))) /. A is Element of the carrier of n

(B |-> (0. n)) /. A is Element of the carrier of n

(B |-> (0. n)) . A is set

n is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

K is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

1. (n,A) is Relation-like NAT -defined the carrier of n * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of A,A, the carrier of n

the carrier of n is non empty non trivial set

the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

(1. (n,A)) . K is Relation-like NAT -defined Function-like V28() FinSequence-like FinSubsequence-like set

(n,A,K) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

0. n is V83(n) Element of the carrier of n

A |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V28() V35(A) FinSequence-like FinSubsequence-like Element of A -tuples_on the carrier of n

A -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

1. n is V83(n) Element of the carrier of n

Replace ((A |-> (0. n)),K,(1. n)) is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

[K,1] is set

Indices (1. (n,A)) is set

dom (1. (n,A)) is Element of bool NAT

width (1. (n,A)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (width (1. (n,A))) is V28() V35( width (1. (n,A))) Element of bool NAT

[:(dom (1. (n,A))),(Seg (width (1. (n,A)))):] is Relation-like set

(1. (n,A)) * (K,1) is Element of the carrier of n

B is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B . 1 is set

len (1. (n,A)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

rng (1. (n,A)) is set

len B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

B . B2 is set

(n,A,K) . B2 is set

[K,B2] is set

(1. (n,A)) * (K,B2) is Element of the carrier of n

(1. (n,A)) * (K,K) is Element of the carrier of n

1_ n is Element of the carrier of n

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B3 . B2 is set

B3 is Relation-like NAT -defined the carrier of n -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B3 . B2 is set

len (n,A,K) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(K,n,A) is Relation-like NAT -defined the carrier of K -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of K

0. K is V83(K) Element of the carrier of K

n |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

n -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

1. K is V83(K) Element of the carrier of K

Replace ((n |-> (0. K)),A,(1. K)) is Relation-like NAT -defined the carrier of K -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of K

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

(1. (K,n)) * (A,B) is Element of the carrier of K

(K,n,A) . B is set

[A,B] is set

Indices (1. (K,n)) is set

dom (1. (K,n)) is Element of bool NAT

width (1. (K,n)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (width (1. (K,n))) is V28() V35( width (1. (K,n))) Element of bool NAT

[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like set

(1. (K,n)) . A is Relation-like NAT -defined Function-like V28() FinSequence-like FinSubsequence-like set

B2 is Relation-like NAT -defined the carrier of K -valued Function-like V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of K

B2 . B is set

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

0. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

n -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

0. K is V83(K) Element of the carrier of K

n |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K

n |-> (n |-> (0. K)) is Relation-like NAT -defined n -tuples_on the carrier of K -valued Function-like V28() V35(n) FinSequence-like FinSubsequence-like Function-yielding V40() Element of n -tuples_on (n -tuples_on the carrier of K)

n -tuples_on (n -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of n -tuples_on the carrier of K

A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

0. (K,n,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A * (B2,B) is Element of the carrier of K

[B2,B] is set

Indices (0. (K,n)) is set

dom (0. (K,n)) is Element of bool NAT

width (0. (K,n)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (width (0. (K,n))) is V28() V35( width (0. (K,n))) Element of bool NAT

[:(dom (0. (K,n))),(Seg (width (0. (K,n)))):] is Relation-like set

(0. (K,n)) + (0. (K,n)) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

((0. (K,n)) + (0. (K,n))) * (B2,B) is Element of the carrier of K

(0. (K,n)) * (B2,B) is Element of the carrier of K

((0. (K,n)) * (B2,B)) + ((0. (K,n)) * (B2,B)) is Element of the carrier of K

the addF of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set

the addF of K . (((0. (K,n)) * (B2,B)),((0. (K,n)) * (B2,B))) is Element of the carrier of K

((0. (K,n)) * (B2,B)) - ((0. (K,n)) * (B2,B)) is Element of the carrier of K

- ((0. (K,n)) * (B2,B)) is Element of the carrier of K

((0. (K,n)) * (B2,B)) + (- ((0. (K,n)) * (B2,B))) is Element of the carrier of K

the addF of K . (((0. (K,n)) * (B2,B)),(- ((0. (K,n)) * (B2,B)))) is Element of the carrier of K

((0. (K,n)) * (B2,B)) + (((0. (K,n)) * (B2,B)) - ((0. (K,n)) * (B2,B))) is Element of the carrier of K

the addF of K . (((0. (K,n)) * (B2,B)),(((0. (K,n)) * (B2,B)) - ((0. (K,n)) * (B2,B)))) is Element of the carrier of K

((0. (K,n)) * (B2,B)) + (0. K) is Element of the carrier of K

the addF of K . (((0. (K,n)) * (B2,B)),(0. K)) is Element of the carrier of K

len A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Indices A is set

dom A is Element of bool NAT

width A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (width A) is V28() V35( width A) Element of bool NAT

[:(dom A),(Seg (width A)):] is Relation-like set

Seg n is V28() V35(n) Element of bool NAT

[:(Seg n),(Seg n):] is Relation-like set

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

[B,B2] is set

A * (B,B2) is Element of the carrier of K

(A * (B,B2)) + (A * (B,B2)) is Element of the carrier of K

the addF of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set

the addF of K . ((A * (B,B2)),(A * (B,B2))) is Element of the carrier of K

B3 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A * (B3,B2) is Element of the carrier of K

A + A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

0. (K,(len A),(width A)) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of len A, width A, the carrier of K

n is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V154() V155() V156() unital V186() V188() right-distributive left-distributive right_unital well-unital V196() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

1. K is V83(K) Element of the carrier of K

0. K is V83(K) Element of the carrier of K

A is Relation-like NAT -defined the carrier of K * -valued Function-like V28() FinSequence-like FinSubsequence-like Function-yielding V40() tabular Matrix of n,n, the carrier of K

Indices A is set

dom A is Element of bool NAT

width A is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Seg (width A) is V28() V35( width A) Element of bool NAT

[:(dom A),(Seg (width A)):] is Relation-like set

Seg n is V28() V35(n) Element of bool NAT

[:(Seg n),(Seg n):] is Relation-like set

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A * (B,B2) is Element of the carrier of K

IFEQ (B,B2,(1. K),(0. K)) is Element of the carrier of K

[B,B2] is set

len (1. (K,n)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

width (1. (K,n)) is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

Indices (1. (K,n)) is set

dom (1. (K,n)) is Element of bool NAT

Seg (width (1. (K,n))) is V28() V35( width (1. (K,n))) Element of bool NAT

[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like set

B is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative set

[B,B2] is set

A * (B,B2) is Element of the carrier of K

(1. (K,n)) * (B,B2) is Element of the carrier of K

B3 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

B2 is V21() V22() V23() V27() V28() V33() V47() V48() ext-real non negative Element of NAT

A * (B3,B2) is Element of the carrier of K

IFEQ (B3,B2,(1. K),(0.