let i be Nat; :: thesis: for D being non empty set
for z being Element of 0 -tuples_on D
for t being Element of i -tuples_on D holds
( z ^ t = t & t ^ z = t )
let D be non empty set ; :: thesis: for z being Element of 0 -tuples_on D
for t being Element of i -tuples_on D holds
( z ^ t = t & t ^ z = t )
let z be Element of 0 -tuples_on D; :: thesis: for t being Element of i -tuples_on D holds
( z ^ t = t & t ^ z = t )
let t be Element of i -tuples_on D; :: thesis: ( z ^ t = t & t ^ z = t )
z = <*> D by Th113;
hence ( z ^ t = t & t ^ z = t ) by FINSEQ_1:47; :: thesis: verum