let uf be FinSequence of F_Real; :: thesis: ( len uf = 3 implies <*uf*> @ = (1. (F_Real,3)) * (<*uf*> @) )
assume A1: len uf = 3 ; :: thesis: <*uf*> @ = (1. (F_Real,3)) * (<*uf*> @)
then A2: <*uf*> @ = <*<*(uf . 1)*>,<*(uf . 2)*>,<*(uf . 3)*>*> by Th63;
then A3: len (<*uf*> @) = 3 by FINSEQ_1:45;
set M = 1. (F_Real,3);
uf is 3 -element by A1, CARD_1:def 7;
then A4: uf in REAL 3 by EUCLID_9:2;

now :: thesis: ( len ((1. (F_Real,3)) * (<*uf*> @)) = 3 & ((1. (F_Real,3)) * (<*uf*> @)) . 1 = <*(uf . 1)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> )

A5: (1. (F_Real,3)) * (<*uf*> @) is Matrix of 3,1,F_Real by A4, EUCLID_8:50, Th74;
hence len ((1. (F_Real,3)) * (<*uf*> @)) = 3 by MATRIX_0:23; :: thesis: ( ((1. (F_Real,3)) * (<*uf*> @)) . 1 = <*(uf . 1)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> )
thus ((1. (F_Real,3)) * (<*uf*> @)) . 1 = <*(uf . 1)*> :: thesis: ( ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> )

proof

1 in Seg 3 by FINSEQ_1:1;
then A6: ((1. (F_Real,3)) * (<*uf*> @)) . 1 = Line (((1. (F_Real,3)) * (<*uf*> @)),1) by A5, MATRIX_0:52;

now :: thesis: ( len (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) = 1 & (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 = uf . 1 )

thus len (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) = width ((1. (F_Real,3)) * (<*uf*> @)) by MATRIX_0:def 7
.= 1 by A5, MATRIX_0:23 ; :: thesis: (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 = uf . 1
thus (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 = uf . 1 :: thesis: verum

proof

A7: [1,1] in Indices ((1. (F_Real,3)) * (<*uf*> @)) by A5, MATRIX_0:23, Th2;
A8: width (1. (F_Real,3)) = len (<*uf*> @) by A3, MATRIX_0:23;
reconsider a1 = 1, a2 = 0 as Element of F_Real ;
A9: ( Line ((1. (F_Real,3)),1) = <*a1,a2,a2*> & uf = <*(uf . 1),(uf . 2),(uf . 3)*> ) by Th56, A1, FINSEQ_1:45;
dom uf = Seg 3 by A1, FINSEQ_1:def 3;
then reconsider uf1 = uf . 1, uf2 = uf . 2, uf3 = uf . 3 as Element of F_Real by FINSEQ_1:1, FINSEQ_2:11;
A10: (Line ((1. (F_Real,3)),1)) "*" uf = ((a1 * uf1) + (a2 * uf2)) + (a2 * uf3) by A9, Th6
.= uf . 1 ;
1 in Seg 1 by FINSEQ_1:1;
then 1 in Seg (width ((1. (F_Real,3)) * (<*uf*> @))) by A5, MATRIX_0:23;
then (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 = ((1. (F_Real,3)) * (<*uf*> @)) * (1,1) by MATRIX_0:def 7
.= (Line ((1. (F_Real,3)),1)) "*" (Col ((<*uf*> @),1)) by A7, A8, MATRIX_3:def 4
.= (Line ((1. (F_Real,3)),1)) "*" uf by Th76 ;
hence (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 = uf . 1 by A10; :: thesis: verum

end;

end;

hence ((1. (F_Real,3)) * (<*uf*> @)) . 1 = <*(uf . 1)*> by A6, FINSEQ_1:40; :: thesis: verum

end;

thus ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> :: thesis: ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*>

proof

2 in Seg 3 by FINSEQ_1:1;
then A11: ((1. (F_Real,3)) * (<*uf*> @)) . 2 = Line (((1. (F_Real,3)) * (<*uf*> @)),2) by A5, MATRIX_0:52;

now :: thesis: ( len (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) = 1 & (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 = uf . 2 )

thus len (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) = width ((1. (F_Real,3)) * (<*uf*> @)) by MATRIX_0:def 7
.= 1 by A5, MATRIX_0:23 ; :: thesis: (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 = uf . 2
thus (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 = uf . 2 :: thesis: verum

proof

A12: [2,1] in Indices ((1. (F_Real,3)) * (<*uf*> @)) by A5, MATRIX_0:23, Th2;
A13: width (1. (F_Real,3)) = len (<*uf*> @) by A3, MATRIX_0:23;
reconsider a1 = 1, a2 = 0 as Element of F_Real ;
A14: ( Line ((1. (F_Real,3)),2) = <*a2,a1,a2*> & uf = <*(uf . 1),(uf . 2),(uf . 3)*> ) by Th56, A1, FINSEQ_1:45;
dom uf = Seg 3 by A1, FINSEQ_1:def 3;
then reconsider uf1 = uf . 1, uf2 = uf . 2, uf3 = uf . 3 as Element of F_Real by FINSEQ_1:1, FINSEQ_2:11;
A15: (Line ((1. (F_Real,3)),2)) "*" uf = ((a2 * uf1) + (a1 * uf2)) + (a2 * uf3) by A14, Th6
.= uf . 2 ;
1 in Seg 1 by FINSEQ_1:1;
then 1 in Seg (width ((1. (F_Real,3)) * (<*uf*> @))) by A5, MATRIX_0:23;
then (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 = ((1. (F_Real,3)) * (<*uf*> @)) * (2,1) by MATRIX_0:def 7
.= (Line ((1. (F_Real,3)),2)) "*" (Col ((<*uf*> @),1)) by A12, A13, MATRIX_3:def 4
.= (Line ((1. (F_Real,3)),2)) "*" uf by Th76 ;
hence (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 = uf . 2 by A15; :: thesis: verum

end;

end;

hence ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> by A11, FINSEQ_1:40; :: thesis: verum

end;

thus ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> :: thesis: verum

proof

3 in Seg 3 by FINSEQ_1:1;
then A16: ((1. (F_Real,3)) * (<*uf*> @)) . 3 = Line (((1. (F_Real,3)) * (<*uf*> @)),3) by A5, MATRIX_0:52;

now :: thesis: ( len (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) = 1 & (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 = uf . 3 )

thus len (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) = width ((1. (F_Real,3)) * (<*uf*> @)) by MATRIX_0:def 7
.= 1 by A5, MATRIX_0:23 ; :: thesis: (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 = uf . 3
thus (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 = uf . 3 :: thesis: verum

proof

A17: [3,1] in Indices ((1. (F_Real,3)) * (<*uf*> @)) by A5, MATRIX_0:23, Th2;
A18: width (1. (F_Real,3)) = len (<*uf*> @) by A3, MATRIX_0:23;
reconsider a1 = 1, a2 = 0 as Element of F_Real ;
A19: ( Line ((1. (F_Real,3)),3) = <*a2,a2,a1*> & uf = <*(uf . 1),(uf . 2),(uf . 3)*> ) by Th56, A1, FINSEQ_1:45;
dom uf = Seg 3 by A1, FINSEQ_1:def 3;
then reconsider uf1 = uf . 1, uf2 = uf . 2, uf3 = uf . 3 as Element of F_Real by FINSEQ_1:1, FINSEQ_2:11;
A20: (Line ((1. (F_Real,3)),3)) "*" uf = ((a2 * uf1) + (a2 * uf2)) + (a1 * uf3) by A19, Th6
.= uf . 3 ;
1 in Seg 1 by FINSEQ_1:1;
then 1 in Seg (width ((1. (F_Real,3)) * (<*uf*> @))) by A5, MATRIX_0:23;
then (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 = ((1. (F_Real,3)) * (<*uf*> @)) * (3,1) by MATRIX_0:def 7
.= (Line ((1. (F_Real,3)),3)) "*" (Col ((<*uf*> @),1)) by A17, A18, MATRIX_3:def 4
.= (Line ((1. (F_Real,3)),3)) "*" uf by Th76 ;
hence (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 = uf . 3 by A20; :: thesis: verum

end;

end;

hence ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> by A16, FINSEQ_1:40; :: thesis: verum

end;

end;

hence <*uf*> @ = (1. (F_Real,3)) * (<*uf*> @) by A2, FINSEQ_1:45; :: thesis: verum