let a, b, c be Real; :: thesis: for N being Matrix of 3,1,F_Real st N = <*<*a*>,<*b*>,<*c*>*> holds
Col (N,1) = <*a,b,c*>
let N be Matrix of 3,1,F_Real; :: thesis: ( N = <*<*a*>,<*b*>,<*c*>*> implies Col (N,1) = <*a,b,c*> )
assume A1: N = <*<*a*>,<*b*>,<*c*>*> ; :: thesis: Col (N,1) = <*a,b,c*>
then A2: ( len N = 3 & N . 1 = <*a*> & N . 2 = <*b*> & N . 3 = <*c*> ) by FINSEQ_1:45;
then A3: dom N = Seg 3 by FINSEQ_1:def 3;
A4: len (Col (N,1)) = len N by MATRIX_0:def 8
.= 3 by A1, FINSEQ_1:45 ;
[1,1] in Indices N by MATRIX_0:23, Th2;
then consider p1 being FinSequence of F_Real such that
A5: p1 = N . 1 and
A6: N * (1,1) = p1 . 1 by MATRIX_0:def 5;
[2,1] in Indices N by MATRIX_0:23, Th2;
then consider p2 being FinSequence of F_Real such that
A8: p2 = N . 2 and
A9: N * (2,1) = p2 . 1 by MATRIX_0:def 5;
A10: N * (2,1) = b by A2, A8, A9, FINSEQ_1:40;
[3,1] in Indices N by MATRIX_0:23, Th2;
then consider p3 being FinSequence of F_Real such that
A11: p3 = N . 3 and
A12: N * (3,1) = p3 . 1 by MATRIX_0:def 5;
A13: N * (3,1) = c by A2, A11, A12, FINSEQ_1:40;
( (Col (N,1)) . 1 = N * (1,1) & (Col (N,1)) . 2 = N * (2,1) & (Col (N,1)) . 3 = N * (3,1) ) by A3, FINSEQ_1:1, MATRIX_0:def 8;
hence Col (N,1) = <*a,b,c*> by A10, A13, A4, A2, A5, A6, FINSEQ_1:40, FINSEQ_1:45; :: thesis: verum