let D be non empty set ; for pf being FinSequence of D
for pr being Element of REAL 3 st pf = pr holds
MXR2MXF (ColVec2Mx pr) = <*pf*> @
let pf be FinSequence of D; for pr being Element of REAL 3 st pf = pr holds
MXR2MXF (ColVec2Mx pr) = <*pf*> @
let pr be Element of REAL 3; ( pf = pr implies MXR2MXF (ColVec2Mx pr) = <*pf*> @ )
assume A1:
pf = pr
; MXR2MXF (ColVec2Mx pr) = <*pf*> @
set M1 = MXR2MXF (ColVec2Mx pr);
set M2 = ColVec2Mx pr;
A2:
MXR2MXF (ColVec2Mx pr) = ColVec2Mx pr
by MATRIXR1:def 1;
pr in REAL 3
;
then A3:
pr in 3 -tuples_on REAL
by EUCLID:def 1;
then A4:
len pr = 3
by FINSEQ_2:133;
A5:
( len (ColVec2Mx pr) = len pr & width (ColVec2Mx pr) = 1 & ( for j being Nat st j in dom pr holds
(ColVec2Mx pr) . j = <*(pr . j)*> ) )
by A4, MATRIXR1:def 9;
now ( len (ColVec2Mx pr) = len (<*pf*> @) & ( for k being Nat st 1 <= k & k <= len (ColVec2Mx pr) holds
(ColVec2Mx pr) . k = (<*pf*> @) . k ) )A6:
width <*pf*> = len pr
by A1, MATRIX_0:23;
hence
len (ColVec2Mx pr) = len (<*pf*> @)
by A5, MATRIX_0:def 6;
for k being Nat st 1 <= k & k <= len (ColVec2Mx pr) holds
(ColVec2Mx pr) . k = (<*pf*> @) . kthus
for
k being
Nat st 1
<= k &
k <= len (ColVec2Mx pr) holds
(ColVec2Mx pr) . k = (<*pf*> @) . k
verumproof
let k be
Nat;
( 1 <= k & k <= len (ColVec2Mx pr) implies (ColVec2Mx pr) . k = (<*pf*> @) . k )
assume that A7:
1
<= k
and A8:
k <= len (ColVec2Mx pr)
;
(ColVec2Mx pr) . k = (<*pf*> @) . k
A9:
k in Seg (len pr)
by A5, A7, A8, FINSEQ_1:1;
then A10:
k in dom pr
by FINSEQ_1:def 3;
A11:
len <*pf*> = 1
by MATRIX_0:23;
A12:
width <*pf*> = 3
by A6, A3, FINSEQ_2:133;
Seg (len (<*pf*> @)) = Seg (len pr)
by A6, MATRIX_0:def 6;
then dom (<*pf*> @) =
Seg (len pr)
by FINSEQ_1:def 3
.=
dom pr
by FINSEQ_1:def 3
;
then A13:
k in dom (<*pf*> @)
by A9, FINSEQ_1:def 3;
then A14:
(<*pf*> @) . k =
Line (
(<*pf*> @),
k)
by MATRIX_0:60
.=
Col (
((<*pf*> @) @),
k)
by A13, MATRIX_0:58
.=
Col (
<*pf*>,
k)
by A12, A11, MATRIX_0:57
.=
<*(pf . k)*>
by A10, A1, Th59
;
k in dom pr
by A9, FINSEQ_1:def 3;
hence
(ColVec2Mx pr) . k = (<*pf*> @) . k
by A4, MATRIXR1:def 9, A1, A14;
verum
end; end;
hence
MXR2MXF (ColVec2Mx pr) = <*pf*> @
by A2, FINSEQ_1:def 17; verum