let n be zero Nat; :: thesis: for X, Y being non empty set
for R being Relation of X,Y holds n -placesOf R = {[{},{}]}
let X, Y be non empty set ; :: thesis: for R being Relation of X,Y holds n -placesOf R = {[{},{}]}
let R be Relation of X,Y; :: thesis: n -placesOf R = {[{},{}]}
set RR = n -placesOf R;
A1: [:(n -tuples_on X),(n -tuples_on Y):] = [:{{}},(0 -tuples_on Y):] by FOMODEL0:10
.= [:{{}},{{}}:] by FOMODEL0:10
.= {[{},{}]} by ZFMISC_1:29 ;
{} in {{}} by TARSKI:def 1;
then reconsider p = {} as Element of n -tuples_on X by FOMODEL0:10;
{} in {{}} by TARSKI:def 1;
then reconsider q = {} as Element of n -tuples_on Y by FOMODEL0:10;
for j being set st j in Seg 0 holds
[(p . j),(q . j)] in R ;
then [p,q] in n -placesOf R ;
then {[{},{}]} c= n -placesOf R by ZFMISC_1:31;
hence n -placesOf R = {[{},{}]} by A1; :: thesis: verum