let n, m be Nat; for I being Function holds Shift ((Shift (I,m)),n) = Shift (I,(m + n))
let I be Function; Shift ((Shift (I,m)),n) = Shift (I,(m + n))
set A = { (l + m) where l is Nat : l in dom I } ;
A1:
dom (Shift (I,m)) = { (l + m) where l is Nat : l in dom I }
by Def12;
A2:
now for l being Nat st l in dom I holds
(Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . llet l be
Nat;
( l in dom I implies (Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . l )assume A3:
l in dom I
;
(Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . lthen A4:
l + m in dom (Shift (I,m))
by A1;
thus (Shift ((Shift (I,m)),n)) . (l + (m + n)) =
(Shift ((Shift (I,m)),n)) . ((l + m) + n)
.=
(Shift (I,m)) . (l + m)
by A4, Def12
.=
I . l
by A3, Def12
;
verum end;
{ (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } } = { (q + (m + n)) where q is Nat : q in dom I }
then
dom (Shift ((Shift (I,m)),n)) = { (l + (m + n)) where l is Nat : l in dom I }
by A1, Def12;
hence
Shift ((Shift (I,m)),n) = Shift (I,(m + n))
by A2, Def12; verum