let a be Int_position; :: thesis: for i being Integer

for n being Nat

for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4

let i be Integer; :: thesis: for n being Nat

for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4

let n be Nat; :: thesis: for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4

let I be Program of ; :: thesis: card (stop (for-up (a,i,n,I))) = (card I) + 4

thus card (stop (for-up (a,i,n,I))) = (card (for-up (a,i,n,I))) + 1 by COMPOS_1:55

.= ((card I) + 3) + 1 by Th30

.= (card I) + 4 ; :: thesis: verum

for n being Nat

for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4

let i be Integer; :: thesis: for n being Nat

for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4

let n be Nat; :: thesis: for I being Program of holds card (stop (for-up (a,i,n,I))) = (card I) + 4

let I be Program of ; :: thesis: card (stop (for-up (a,i,n,I))) = (card I) + 4

thus card (stop (for-up (a,i,n,I))) = (card (for-up (a,i,n,I))) + 1 by COMPOS_1:55

.= ((card I) + 3) + 1 by Th30

.= (card I) + 4 ; :: thesis: verum