let c1, c2, c3, c4 be Complex; :: thesis: <*c1,c2,c3,c4*> " = <*(c1 "),(c2 "),(c3 "),(c4 ")*>
<*c4*> " = <*(c4 ")*> by NUMBER15:63;
hence <*(c1 "),(c2 "),(c3 "),(c4 ")*> = (<*c1,c2,c3*> ") ^ (<*c4*> ") by NUMBER15:65
.= <*c1,c2,c3,c4*> " by NUMBER15:60 ;
:: thesis: verum