let c1, c2, c3, c4, c5, c6, c7 be Complex; :: thesis: <*c1,c2,c3,c4,c5,c6,c7*> " = <*(c1 "),(c2 "),(c3 "),(c4 "),(c5 "),(c6 "),(c7 ")*>
<*c6,c7*> " = <*(c6 "),(c7 ")*> by NUMBER15:64;
hence <*(c1 "),(c2 "),(c3 "),(c4 "),(c5 "),(c6 "),(c7 ")*> = (<*c1,c2,c3,c4,c5*> ") ^ (<*c6,c7*> ") by Th16
.= <*c1,c2,c3,c4,c5,c6,c7*> " by NUMBER15:60 ;
:: thesis: verum