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

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