let n be Element of NAT ; :: thesis: for I being NAT -defined finite initial Function
for J being Function holds dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
let I be NAT -defined finite initial Function; :: thesis: for J being Function holds dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
let J be Function; :: thesis: dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
assume A1: dom (Shift (I,n)) meets dom (Shift (J,(n + (card I)))) ; :: thesis: contradiction
dom (Shift (J,(n + (card I)))) = { (l + (n + (card I))) where l is Element of NAT : l in dom J } by VALUED_1:def 12;
then consider x being set such that
A2: x in dom (Shift (I,n)) and
A3: x in { (l + (n + (card I))) where l is Element of NAT : l in dom J } by A1, XBOOLE_0:3;
dom (Shift (I,n)) = { (m + n) where m is Element of NAT : m in dom I } by VALUED_1:def 12;
then consider m being Element of NAT such that
W1: x = m + n and
W2: m in dom I by A2;
consider l being Element of NAT such that
A4: x = l + (n + (card I)) and
l in dom J by A3;
m < card I by W2, Th70;
then m + n < n + (card I) by XREAL_1:8;
then l + (n + (card I)) < n + (card I) by W1, A4;
hence contradiction by NAT_1:11; :: thesis: verum