let I be NAT -defined finite initial Function; :: thesis: for J being Function holds dom I misses dom (Shift (J,(card I)))
let J be Function; :: thesis: dom I misses dom (Shift (J,(card I)))
assume A1: dom I meets dom (Shift (J,(card I))) ; :: thesis: contradiction
dom (Shift (J,(card I))) = { (l + (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 I and
A3: x in { (l + (card I)) where l is Nat : l in dom J } by A1, XBOOLE_0:3;
consider l being Nat such that
A4: x = l + (card I) and
l in dom J by A3;
thus contradiction by NAT_1:11, A2, A4, Lm1; :: thesis: verum