let i be Element of 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 10;
hence ( i in dom f implies f /. i in L~ f ) by GOBOARD1:16; :: thesis: verum