let i be Nat; for x, y being set
for f being NAT -defined non empty finite Function holds Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)
let x, y be set ; for f being NAT -defined non empty finite Function holds Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)
let f be NAT -defined non empty finite Function; Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)
A1:
dom f = dom (f +~ (x,y))
by FUNCT_4:99;
A2: dom ((Shift (f,i)) +~ (x,y)) =
dom (Shift (f,i))
by FUNCT_4:99
.=
{ (m + i) where m is Nat : m in dom (f +~ (x,y)) }
by A1, Def12
;
for m being Nat st m in dom (f +~ (x,y)) holds
((Shift (f,i)) +~ (x,y)) . (m + i) = (f +~ (x,y)) . m
proof
let m be
Nat;
( m in dom (f +~ (x,y)) implies ((Shift (f,i)) +~ (x,y)) . (m + i) = (f +~ (x,y)) . m )
assume
m in dom (f +~ (x,y))
;
((Shift (f,i)) +~ (x,y)) . (m + i) = (f +~ (x,y)) . m
then A3:
m + i in dom ((Shift (f,i)) +~ (x,y))
by A2;
then A4:
m + i in dom (Shift (f,i))
by FUNCT_4:99;
consider mm being
Nat such that A5:
m + i = mm + i
and A6:
mm in dom (f +~ (x,y))
by A2, A3;
m = mm
by A5;
then
m in dom (f +~ (x,y))
by A6;
then A7:
m in dom f
by FUNCT_4:99;
then A8:
(Shift (f,i)) . (m + i) = f . m
by Def12;
end;
hence
Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)
by A2, Def12; verum