let a, b, c, d, x, y, z, v be Complex; :: thesis: <*a,b,c,d*> (#) <*x,y,z,v*> = <*(a * x),(b * y),(c * z),(d * v)*>
reconsider f = <*a,b,c*> as 3 -element complex-valued FinSequence ;
reconsider g = <*x,y,z*> as 3 -element complex-valued FinSequence ;
( <*a,b,c,d*> = f ^ <*d*> & <*x,y,z,v*> = g ^ <*v*> ) by FINSEQ_4:def 7;
then <*a,b,c,d*> (#) <*x,y,z,v*> = (f (#) g) ^ <*(d * v)*> by FMA
.= <*(a * x),(b * y),(c * z)*> ^ <*(d * v)*> by AM3 ;
hence <*a,b,c,d*> (#) <*x,y,z,v*> = <*(a * x),(b * y),(c * z),(d * v)*> by FINSEQ_4:def 7; :: thesis: verum