let q be FinSubsequence; :: thesis: 0 Shift q = q
set X = { (0 + k) where k is Element of NAT : k in dom q } ;
A1: dom (0 Shift q) = { (0 + k) where k is Element of NAT : k in dom q } by Def15;
A2: { (0 + k) where k is Element of NAT : k in dom q } = dom q

proof

thus { (0 + k) where k is Element of NAT : k in dom q } c= dom q :: according to XBOOLE_0:def 10 :: thesis: dom q c= { (0 + k) where k is Element of NAT : k in dom q }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (0 + k) where k is Element of NAT : k in dom q } or x in dom q )
assume x in { (0 + k) where k is Element of NAT : k in dom q } ; :: thesis: x in dom q
then ex k being Element of NAT st
( x = 0 + k & k in dom q ) ;
hence x in dom q ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom q or x in { (0 + k) where k is Element of NAT : k in dom q } )
assume A3: x in dom q ; :: thesis: x in { (0 + k) where k is Element of NAT : k in dom q }
consider l being Nat such that
A4: dom q c= Seg l by FINSEQ_1:def 12;
x in Seg l by A3, A4;
then reconsider k = x as Element of NAT ;
x = 0 + k ;
hence x in { (0 + k) where k is Element of NAT : k in dom q } by A3; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { (0 + k) where k is Element of NAT : k in dom q } implies (0 Shift q) . x = q . x )
assume x in { (0 + k) where k is Element of NAT : k in dom q } ; :: thesis: (0 Shift q) . x = q . x
then ex k being Element of NAT st
( x = 0 + k & k in dom q ) ;
hence (0 Shift q) . x = q . x by Def15; :: thesis: verum

end;

hence 0 Shift q = q by A1, A2, FUNCT_1:2; :: thesis: verum