let R be Ring; :: thesis: for pf being FinSequence of R
for N being Matrix of 3,R st len pf = 3 holds
( Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> & Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> & Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> )
let pf be FinSequence of R; :: thesis: for N being Matrix of 3,R st len pf = 3 holds
( Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> & Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> & Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> )
let N be Matrix of 3,R; :: thesis: ( len pf = 3 implies ( Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> & Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> & Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> ) )
assume len pf = 3 ; :: thesis: ( Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> & Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> & Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> )
then N * (<*pf*> @) is Matrix of 3,1,R by Th74;
hence ( Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> & Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> & Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> ) by Th73; :: thesis: verum