let X be non empty set ; :: thesis: for s, s1 being sequence of X st s is constant & s1 is subsequence of s holds
s = s1
let s, s1 be sequence of X; :: thesis: ( s is constant & s1 is subsequence of s implies s = s1 )
assume that
A1: s is constant and
A2: s1 is subsequence of s ; :: thesis: s = s1
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: s . n = s1 . n
consider N being increasing sequence of NAT such that
A3: s1 = s * N by A2, Def13;
thus s1 . n = s . (N . n) by A3, FUNCT_2:15
.= s . n by A1, Th23 ; :: thesis: verum