let i be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: ((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;

per cases ( (Shift (f,i)) . (m + i) = x or (Shift (f,i)) . (m + i) <> x ) ;

suppose A9: (Shift (f,i)) . (m + i) = x ; :: thesis: ((Shift (f,i)) +~ (x,y)) . (m + i) = (f +~ (x,y)) . m

hence ((Shift (f,i)) +~ (x,y)) . (m + i) = y by A4, FUNCT_4:106
.= (f +~ (x,y)) . m by A7, FUNCT_4:106, A9, A8 ;
:: thesis: verum

end;

suppose A10: (Shift (f,i)) . (m + i) <> x ; :: thesis: ((Shift (f,i)) +~ (x,y)) . (m + i) = (f +~ (x,y)) . m

hence ((Shift (f,i)) +~ (x,y)) . (m + i) = (Shift (f,i)) . (m + i) by FUNCT_4:105
.= (f +~ (x,y)) . m by A10, A8, FUNCT_4:105 ;
:: thesis: verum

end;

end;

end;

hence Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y) by A2, Def12; :: thesis: verum