let k1, k2, k3, k4 be Instruction of SCM+FSA ; :: thesis: card (((k1 ';' k2) ';' k3) ';' k4) = 8
thus card (((k1 ';' k2) ';' k3) ';' k4) = (card ((k1 ';' k2) ';' k3)) + (card (Macro k4)) by SCMFSA6A:61
.= (card ((k1 ';' k2) ';' k3)) + 2 by SCMFSA7B:6
.= 6 + 2 by SCMBSORT:45
.= 8 ; :: thesis: verum