let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] ) assume A4:
S1[k]
; :: thesis: S1[k + 1] set Fwk = { (F . w) where w is Element of NAT : ( A <= w & w <= A + k ) } ; reconsider Fwk = { (F . w) where w is Element of NAT : ( A <= w & w <= A + k ) } as finitesetbyA4; set Fwk1 = { (F . w) where w is Element of NAT : ( A <= w & w <=(A + k)+ 1 ) } ;