let n be 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 Nat : l in dom J } by VALUED_1:def 12;
then consider x being object such that
A2: x in dom (Shift (I,n)) and
A3: x in { (l + (n + (card I))) where l is Nat : l in dom J } by A1, XBOOLE_0:3;
dom (Shift (I,n)) = { (m + n) where m is Nat : m in dom I } by VALUED_1:def 12;
then consider m being Nat such that
A4: x = m + n and
A5: m in dom I by A2;
consider l being Nat such that
A6: x = l + (n + (card I)) and
l in dom J by A3;
m < card I by A5, Lm1;
hence contradiction by NAT_1:11, A4, A6, XREAL_1:6; :: thesis: verum