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