let i be Nat; :: thesis: for f being S-Sequence_in_R2 st i in dom f holds
f /. i in L~ f
let f be S-Sequence_in_R2; :: thesis: ( i in dom f implies f /. i in L~ f )
len f >= 2 by TOPREAL1:def 8;
hence ( i in dom f implies f /. i in L~ f ) by GOBOARD1:1; :: thesis: verum