let X be non empty set ; :: thesis: for s being sequence of X
for n, m being Nat st m + 1 in dom (Shift ((s | (Segm n)),1)) holds
(Shift ((s | (Segm n)),1)) . (m + 1) = s . m
let s be sequence of X; :: thesis: for n, m being Nat st m + 1 in dom (Shift ((s | (Segm n)),1)) holds
(Shift ((s | (Segm n)),1)) . (m + 1) = s . m
let n, m be Nat; :: thesis: ( m + 1 in dom (Shift ((s | (Segm n)),1)) implies (Shift ((s | (Segm n)),1)) . (m + 1) = s . m )
assume m + 1 in dom (Shift ((s | (Segm n)),1)) ; :: thesis: (Shift ((s | (Segm n)),1)) . (m + 1) = s . m
then consider k being Nat such that
A1: ( k in dom (s | (Segm n)) & m + 1 = k + 1 ) by VALUED_1:39;
(Shift ((s | (Segm n)),1)) . (m + 1) = (s | (Segm n)) . m by A1, VALUED_1:def 12;
hence (Shift ((s | (Segm n)),1)) . (m + 1) = s . m by A1, FUNCT_1:47; :: thesis: verum