let V1, V2 be Subset of ((n + k) -tuples_on {A,B}); :: thesis: ( ( for v being Element of (n + k) -tuples_on {A,B} holds
( v in V1 iff card (v " {A}) = n ) ) & ( for v being Element of (n + k) -tuples_on {A,B} holds
( v in V2 iff card (v " {A}) = n ) ) implies V1 = V2 )
assume that
A1: for v being Element of (n + k) -tuples_on {A,B} holds
( v in V1 iff card (v " {A}) = n ) and
A2: for v being Element of (n + k) -tuples_on {A,B} holds
( v in V2 iff card (v " {A}) = n ) ; :: thesis: V1 = V2

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: V2 c= V1

let x be object ; :: thesis: ( x in V1 implies x in V2 )
assume A3: x in V1 ; :: thesis: x in V2
then reconsider v = x as Element of (n + k) -tuples_on {A,B} ;
card (v " {A}) = n by A1, A3;
hence x in V2 by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V2 or x in V1 )
assume A4: x in V2 ; :: thesis: x in V1
then reconsider v = x as Element of (n + k) -tuples_on {A,B} ;
card (v " {A}) = n by A2, A4;
hence x in V1 by A1; :: thesis: verum