thus card (((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1)) ';' (SubFrom GBP ,3,GBP ,2)) = (card ((if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1))) ';' (GBP ,3 := GBP ,1))) + 1 by SCMP_GCD:8
.= ((card (if>0 GBP ,3,(Load (SubFrom GBP ,1,GBP ,2)),(Load (SubFrom GBP ,2,GBP ,1)))) + 1) + 1 by SCMP_GCD:8
.= ((((card (Load (SubFrom GBP ,1,GBP ,2))) + (card (Load (SubFrom GBP ,2,GBP ,1)))) + 2) + 1) + 1 by SCMPDS_6:79
.= (((1 + (card (Load (SubFrom GBP ,2,GBP ,1)))) + 2) + 1) + 1 by SCMPDS_5:6
.= (((1 + 1) + 2) + 1) + 1 by SCMPDS_5:6
.= 6 ; :: thesis: verum