let x be set ; :: thesis: for f1, f2 being FinSequence st not x in rng f1 holds
x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1
let f1, f2 be FinSequence; :: thesis: ( not x in rng f1 implies x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1 )
x in {x} by TARSKI:def 1;
then A1: x in rng <*x*> by FINSEQ_1:38;
assume not x in rng f1 ; :: thesis: x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1
then x in (rng <*x*>) \ (rng f1) by A1, XBOOLE_0:def 5;
then A2: (f1 ^ <*x*>) |-- x = <*x*> |-- x by Th9
.= {} by Th32 ;
rng (f1 ^ <*x*>) = (rng f1) \/ (rng <*x*>) by FINSEQ_1:31;
then A3: x in rng (f1 ^ <*x*>) by A1, XBOOLE_0:def 3;
then (len (f1 ^ <*x*>)) - (x .. (f1 ^ <*x*>)) = len ((f1 ^ <*x*>) |-- x) by FINSEQ_4:def 6
.= 0 by A2 ;
hence x .. ((f1 ^ <*x*>) ^ f2) = len (f1 ^ <*x*>) by A3, Th6
.= (len f1) + (len <*x*>) by FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
:: thesis: verum