thus card (((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))) = (card ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4)))) + 1 by SCMP_GCD:8
.= ((card (((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1)))) + 1) + 1 by SCMP_GCD:8
.= (2 + 1) + 1 by SCMP_GCD:9
.= 4 ; :: thesis: verum