let f be FinSequence of NAT ; :: thesis: for j, b being Nat st b = j holds
(f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)}
let j, b be Nat; :: thesis: ( b = j implies (f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)} )
assume A130: b = j ; :: thesis: (f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)}
for z being object holds
( z in (f ^ <*b*>) " {j} iff z in (f " {j}) \/ {((len f) + 1)} )

proof

let z be object ; :: thesis: ( z in (f ^ <*b*>) " {j} iff z in (f " {j}) \/ {((len f) + 1)} )

hereby :: thesis: ( z in (f " {j}) \/ {((len f) + 1)} implies z in (f ^ <*b*>) " {j} )

assume A200: z in (f ^ <*b*>) " {j} ; :: thesis: z in (f " {j}) \/ {((len f) + 1)}
then ( z in dom (f ^ <*b*>) & (f ^ <*b*>) . z in {j} ) by FUNCT_1:def 7;

per cases then ( z in dom f or ex n being Nat st
( n in dom <*b*> & z = (len f) + n ) ) by FINSEQ_1:25;

suppose B00: z in dom f ; :: thesis: z in (f " {j}) \/ {((len f) + 1)}

then (f ^ <*b*>) . z = f . z by FINSEQ_1:def 7;
then f . z in {j} by A200, FUNCT_1:def 7;
then z in f " {j} by B00, FUNCT_1:def 7;
hence z in (f " {j}) \/ {((len f) + 1)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom <*b*> & z = (len f) + n ) ; :: thesis: z in (f " {j}) \/ {((len f) + 1)}

then consider n1 being Nat such that
B60: ( n1 in dom <*b*> & z = (len f) + n1 ) ;
n1 = 1 by B60, FINSEQ_1:90;
then z in {((len f) + 1)} by B60, TARSKI:def 1;
hence z in (f " {j}) \/ {((len f) + 1)} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume z in (f " {j}) \/ {((len f) + 1)} ; :: thesis: z in (f ^ <*b*>) " {j}
then ( z in f " {j} or z in {((len f) + 1)} ) by XBOOLE_0:def 3;

per cases then ( ( z in dom f & f . z in {j} ) or z in {((len f) + 1)} ) by FUNCT_1:def 7;

suppose B00: ( z in dom f & f . z in {j} ) ; :: thesis: z in (f ^ <*b*>) " {j}

A319: dom f c= dom (f ^ <*b*>) by FINSEQ_1:26;
(f ^ <*b*>) . z in {j} by B00, FINSEQ_1:def 7;
hence z in (f ^ <*b*>) " {j} by A319, B00, FUNCT_1:def 7; :: thesis: verum

end;

suppose z in {((len f) + 1)} ; :: thesis: z in (f ^ <*b*>) " {j}

then B60: z = (len f) + 1 by TARSKI:def 1;
dom <*b*> = {1} by FINSEQ_1:def 8, FINSEQ_1:2;
then 1 in dom <*b*> by TARSKI:def 1;
then B69: (len f) + 1 in dom (f ^ <*b*>) by FINSEQ_1:28;
(f ^ <*b*>) . z = j by B60, FINSEQ_1:42, A130;
then (f ^ <*b*>) . z in {j} by ZFMISC_1:31;
hence z in (f ^ <*b*>) " {j} by B69, B60, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

hence (f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)} by TARSKI:2; :: thesis: verum