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 )
assume dom R c= n -tuples_on D ; :: thesis: R is homogeneous
hence dom R is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum