let a be non zero Element of F_Real; :: thesis: for uf being FinSequence of F_Real st len uf = 3 holds
(a * (1. (F_Real,3))) * (<*uf*> @) = a * (<*uf*> @)
let uf be FinSequence of F_Real; :: thesis: ( len uf = 3 implies (a * (1. (F_Real,3))) * (<*uf*> @) = a * (<*uf*> @) )
assume A1: len uf = 3 ; :: thesis: (a * (1. (F_Real,3))) * (<*uf*> @) = a * (<*uf*> @)
width <*uf*> = 3 by A1, MATRIX_0:23;
then len (<*uf*> @) = 3 by MATRIX_0:29;
then width (1. (F_Real,3)) = len (<*uf*> @) by MATRIX_0:23;
then (a * (1. (F_Real,3))) * (<*uf*> @) = a * ((1. (F_Real,3)) * (<*uf*> @)) by MATRIX15:1;
hence (a * (1. (F_Real,3))) * (<*uf*> @) = a * (<*uf*> @) by A1, ANPROJ_8:99; :: thesis: verum