let x, y be set ; :: thesis: for f being FinSequence st x in rng f & y in rng (f -| x) holds
(f -| x) -| y = f -| y
let f be FinSequence; :: thesis: ( x in rng f & y in rng (f -| x) implies (f -| x) -| y = f -| y )
assume that
A1: x in rng f and
A2: y in rng (f -| x) ; :: thesis: (f -| x) -| y = f -| y
thus f -| y = (((f -| x) ^ <*x*>) ^ (f |-- x)) -| y by A1, FINSEQ_4:51
.= ((f -| x) ^ (<*x*> ^ (f |-- x))) -| y by FINSEQ_1:32
.= (f -| x) -| y by A2, Th12 ; :: thesis: verum