let R be Ring; for N being Matrix of 3,R
for p being FinSequence of R st len p = 3 holds
N * (<*p*> @) is 3,1 -size
let N be Matrix of 3,R; for p being FinSequence of R st len p = 3 holds
N * (<*p*> @) is 3,1 -size
let p be FinSequence of R; ( len p = 3 implies N * (<*p*> @) is 3,1 -size )
assume A1:
len p = 3
; N * (<*p*> @) is 3,1 -size
then A2:
width <*p*> = 3
by MATRIX_0:23;
then A3: width N =
width <*p*>
by MATRIX_0:24
.=
len (<*p*> @)
by MATRIX_0:def 6
;
now ( len (N * (<*p*> @)) = 3 & ( for pf being FinSequence of R st pf in rng (N * (<*p*> @)) holds
len pf = 1 ) )
len (N * (<*p*> @)) = len N
by A3, MATRIX_3:def 4;
hence A4:
len (N * (<*p*> @)) = 3
by MATRIX_0:24;
for pf being FinSequence of R st pf in rng (N * (<*p*> @)) holds
len pf = 1thus
for
pf being
FinSequence of
R st
pf in rng (N * (<*p*> @)) holds
len pf = 1
verumproof
let pf be
FinSequence of
R;
( pf in rng (N * (<*p*> @)) implies len pf = 1 )
assume A5:
pf in rng (N * (<*p*> @))
;
len pf = 1
A6:
len <*p*> = 1
by MATRIX_0:23;
A7:
width <*p*> = 3
by A1, MATRIX_0:23;
A8:
width N =
width <*p*>
by A2, MATRIX_0:24
.=
len (<*p*> @)
by MATRIX_0:def 6
;
A9:
width (<*p*> @) =
len ((<*p*> @) @)
by MATRIX_0:def 6
.=
1
by A6, A7, MATRIX_0:57
;
consider s being
FinSequence such that A10:
s in rng (N * (<*p*> @))
and A11:
len s = width (N * (<*p*> @))
by A4, MATRIX_0:def 3;
consider n0 being
Nat such that A12:
for
x being
object st
x in rng (N * (<*p*> @)) holds
ex
s being
FinSequence st
(
s = x &
len s = n0 )
by MATRIX_0:def 1;
A13:
ex
s0 being
FinSequence st
(
s0 = pf &
len s0 = n0 )
by A12, A5;
ex
s1 being
FinSequence st
(
s1 = s &
len s1 = n0 )
by A10, A12;
hence
len pf = 1
by A9, A8, MATRIX_3:def 4, A11, A13;
verum
end; end;
hence
N * (<*p*> @) is 3,1 -size
by MATRIX_0:def 2; verum