let D be set ; :: thesis: for z being Element of 0 -tuples_on D holds z = <*> D
let z be Element of 0 -tuples_on D; :: thesis: z = <*> D
0 -tuples_on D = {(<*> D)} by Th112;
hence z = <*> D by TARSKI:def 1; :: thesis: verum