let n be Nat; 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; for J being Function holds dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
let J be Function; dom (Shift (I,n)) misses dom (Shift (J,(n + (card I))))
assume A1:
dom (Shift (I,n)) meets dom (Shift (J,(n + (card I))))
; 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; verum