set A = { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } ;
{ (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } c= V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } or x in V )
assume x in { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } ; :: thesis: x in V
then ex k being Nat st
( l . k = x & 1 <= k & k <= len l & l . k in V ) ;
hence x in V ; :: thesis: verum

end;

hence { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } is Subset of V ; :: thesis: verum