let n be Nat; :: thesis: for i being Instruction of SCMPDS
for I, J being Program of holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
let i be Instruction of SCMPDS; :: thesis: for I, J being Program of holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
let I, J be Program of ; :: thesis: card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
set G = Goto n;
thus card (((i ';' I) ';' (Goto n)) ';' J) = (card ((i ';' I) ';' (Goto n))) + (card J) by AFINSQ_1:17
.= ((card (i ';' I)) + (card (Goto n))) + (card J) by AFINSQ_1:17
.= ((card (i ';' I)) + 1) + (card J) by COMPOS_1:54
.= (((card I) + 1) + 1) + (card J) by Th1
.= ((card I) + (card J)) + 2 ; :: thesis: verum