let R be Ring; :: thesis: 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; :: thesis: for p being FinSequence of R st len p = 3 holds
N * (<*p*> @) is 3,1 -size
let p be FinSequence of R; :: thesis: ( len p = 3 implies N * (<*p*> @) is 3,1 -size )
assume A1: len p = 3 ; :: thesis: 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 :: thesis: ( 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; :: thesis: for pf being FinSequence of R st pf in rng (N * (<*p*> @)) holds
len pf = 1
thus for pf being FinSequence of R st pf in rng (N * (<*p*> @)) holds
len pf = 1 :: thesis: verum

proof

let pf be FinSequence of R; :: thesis: ( pf in rng (N * (<*p*> @)) implies len pf = 1 )
assume A5: pf in rng (N * (<*p*> @)) ; :: thesis: 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; :: thesis: verum

end;

end;

hence N * (<*p*> @) is 3,1 -size by MATRIX_0:def 2; :: thesis: verum