let n be Element of NAT ; :: thesis: for D being non empty set
for R being Relation st dom R c= n -tuples_on D holds
R is homogeneous
let D be non empty set ; :: thesis: for R being Relation st dom R c= n -tuples_on D holds
R is homogeneous
let R be Relation; :: thesis: ( dom R c= n -tuples_on D implies R is homogeneous )
set X = D;
assume A1: dom R c= n -tuples_on D ; :: thesis: R is homogeneous
let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom R or not y in dom R or len x = len y )
assume A2: ( x in dom R & y in dom R ) ; :: thesis: len x = len y
reconsider x' = x, y' = y as Element of n -tuples_on D by A1, A2;
( len x' = n & len y' = n ) by FINSEQ_1:def 18;
hence len x = len y ; :: thesis: verum