let n be Nat; :: thesis: for X being non empty set
for s being sequence of X holds s . n in rng s
let X be non empty set ; :: thesis: for s being sequence of X holds s . n in rng s
let s be sequence of X; :: thesis: s . n in rng s
n in NAT by ORDINAL1:def 12;
then n in dom s by FUNCT_2:def 1;
hence s . n in rng s by FUNCT_1:3; :: thesis: verum