let a be Real; for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
M2F (a * p) = a * (M2F p)
let p be FinSequence of 1 -tuples_on REAL; ( len p = 3 implies M2F (a * p) = a * (M2F p) )
assume A1:
len p = 3
; M2F (a * p) = a * (M2F p)
then consider p1, p2, p3 being Real such that
A2:
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 )
and
A3:
a * p = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*>
by DEF3;
( (a * p) . 1 = <*(a * p1)*> & (a * p) . 2 = <*(a * p2)*> & (a * p) . 3 = <*(a * p3)*> )
by A3, FINSEQ_1:45;
then A4:
( ((a * p) . 1) . 1 = a * p1 & ((a * p) . 2) . 1 = a * p2 & ((a * p) . 3) . 1 = a * p3 )
by FINSEQ_1:40;
len (a * p) = 3
by A3, FINSEQ_1:45;
then A5:
M2F (a * p) = |[(a * p1),(a * p2),(a * p3)]|
by A4, DEF2;
reconsider q = M2F p as FinSequence of F_Real ;
M2F p = |[p1,p2,p3]|
by A1, A2, DEF2;
hence
M2F (a * p) = a * (M2F p)
by A5, EUCLID_8:59; verum