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

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