let n be Element of NAT ; :: thesis: for i being Instruction of
for I, J being Program of holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2
let i be Instruction of ; :: 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 SCMPDS_4:45
.= ((card (i ';' I)) + (card (Goto n))) + (card J) by SCMPDS_4:45
.= ((card (i ';' I)) + 1) + (card J) by SCMPDS_5:6
.= (((card I) + 1) + 1) + (card J) by Th15
.= ((card I) + (card J)) + 2 ; :: thesis: verum