set V = { v where v is Element of (n + k) -tuples_on {A,B} : card (v " {A}) = n } ;
{ v where v is Element of (n + k) -tuples_on {A,B} : card (v " {A}) = n } c= (n + k) -tuples_on {A,B}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (n + k) -tuples_on {A,B} : card (v " {A}) = n } or x in (n + k) -tuples_on {A,B} )
assume x in { v where v is Element of (n + k) -tuples_on {A,B} : card (v " {A}) = n } ; :: thesis: x in (n + k) -tuples_on {A,B}
then ex v being Element of (n + k) -tuples_on {A,B} st
( v = x & card (v " {A}) = n ) ;
hence x in (n + k) -tuples_on {A,B} ; :: thesis: verum

end;

then reconsider V = { v where v is Element of (n + k) -tuples_on {A,B} : card (v " {A}) = n } as Subset of ((n + k) -tuples_on {A,B}) ;
take V ; :: thesis: for v being Element of (n + k) -tuples_on {A,B} holds
( v in V iff card (v " {A}) = n )
let v be Element of (n + k) -tuples_on {A,B}; :: thesis: ( v in V iff card (v " {A}) = n )

hereby :: thesis: ( card (v " {A}) = n implies v in V )

assume v in V ; :: thesis: card (v " {A}) = n
then ex v1 being Element of (n + k) -tuples_on {A,B} st
( v = v1 & card (v1 " {A}) = n ) ;
hence card (v " {A}) = n ; :: thesis: verum

end;

thus ( card (v " {A}) = n implies v in V ) ; :: thesis: verum