let n be non zero Nat; :: thesis: for D being non empty set

for p being Element of n -tuples_on D holds

( len p = n & p is Element of D * )

let D be non empty set ; :: thesis: for p being Element of n -tuples_on D holds

( len p = n & p is Element of D * )

let p be Element of n -tuples_on D; :: thesis: ( len p = n & p is Element of D * )

p in n -tuples_on D ;

then ex s being Element of D * st

( p = s & len s = n ) ;

hence ( len p = n & p is Element of D * ) ; :: thesis: verum

for p being Element of n -tuples_on D holds

( len p = n & p is Element of D * )

let D be non empty set ; :: thesis: for p being Element of n -tuples_on D holds

( len p = n & p is Element of D * )

let p be Element of n -tuples_on D; :: thesis: ( len p = n & p is Element of D * )

p in n -tuples_on D ;

then ex s being Element of D * st

( p = s & len s = n ) ;

hence ( len p = n & p is Element of D * ) ; :: thesis: verum