let x, y be FinSequence of COMPLEX ; :: thesis: for M being Matrix of COMPLEX st len x = len M & len y = width M & width M > 0 & len M > 0 holds
|(x,(M * y))| = |(((M @") * x),y)|
let M be Matrix of COMPLEX; :: thesis: ( len x = len M & len y = width M & width M > 0 & len M > 0 implies |(x,(M * y))| = |(((M @") * x),y)| )
assume that
A1: len x = len M and
A2: len y = width M and
A3: width M > 0 and
A4: len M > 0 ; :: thesis: |(x,(M * y))| = |(((M @") * x),y)|
A5: len ((M @") * x) = len (M @") by Def6
.= len (M @) by Def1
.= width M by MATRIX_0:def 6 ;
len (M * y) = len x by A1, Def6;
hence |(x,(M * y))| = |((M * y),x)| *' by A1, A4, Th52
.= |(y,((M @") * x))| *' by A1, A2, A3, A4, Th57
.= |(((M @") * x),y)| by A2, A3, A5, Th52 ;
:: thesis: verum