let D be set ; :: thesis: 0 -tuples_on D = {(<*> D)}

now :: thesis: for z being object holds
( ( z in 0 -tuples_on D implies z = <*> D ) & ( z = <*> D implies z in 0 -tuples_on D ) )

let z be object ; :: thesis: ( ( z in 0 -tuples_on D implies z = <*> D ) & ( z = <*> D implies z in 0 -tuples_on D ) )
thus ( z in 0 -tuples_on D implies z = <*> D ) :: thesis: ( z = <*> D implies z in 0 -tuples_on D )

proof

assume z in 0 -tuples_on D ; :: thesis: z = <*> D
then ex s being Element of D * st
( z = s & len s = 0 ) ;
hence z = <*> D ; :: thesis: verum

end;

( <*> D is Element of D * & len (<*> D) = 0 ) by FINSEQ_1:def 11;
hence ( z = <*> D implies z in 0 -tuples_on D ) ; :: thesis: verum

end;

hence 0 -tuples_on D = {(<*> D)} by TARSKI:def 1; :: thesis: verum