let D be non empty set ; :: thesis: for d being Element of D
for p being FinSequence of D holds rng ([#] p,d) = (rng p) \/ {d}
let d be Element of D; :: thesis: for p being FinSequence of D holds rng ([#] p,d) = (rng p) \/ {d}
let p be FinSequence of D; :: thesis: rng ([#] p,d) = (rng p) \/ {d}

now

let y be set ; :: thesis: ( ( y in rng ([#] p,d) implies y in (rng p) \/ {d} ) & ( y in (rng p) \/ {d} implies y in rng ([#] p,d) ) )
thus ( y in rng ([#] p,d) implies y in (rng p) \/ {d} ) :: thesis: ( y in (rng p) \/ {d} implies y in rng ([#] p,d) )

proof

assume y in rng ([#] p,d) ; :: thesis: y in (rng p) \/ {d}
then consider x being set such that
A1: x in dom ([#] p,d) and
A2: y = ([#] p,d) . x by FUNCT_1:def 5;
reconsider i = x as Element of NAT by A1;

now

per cases ( i in dom p or not i in dom p ) ;

case A3: i in dom p ; :: thesis: y in rng p

then y = p . i by A2, Th22;
hence y in rng p by A3, FUNCT_1:def 5; :: thesis: verum

end;

case not i in dom p ; :: thesis: y in {d}

then y = d by A2, Th22;
hence y in {d} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence y in (rng p) \/ {d} by XBOOLE_0:def 3; :: thesis: verum

end;

assume A4: y in (rng p) \/ {d} ; :: thesis: y in rng ([#] p,d)

now

per cases ( y in rng p or y in {d} ) by A4, XBOOLE_0:def 3;

suppose y in rng p ; :: thesis: y in rng ([#] p,d)

then consider i being Nat such that
A5: i in dom p and
A6: y = p . i by FINSEQ_2:11;
y = ([#] p,d) . i by A5, A6, Th22;
hence y in rng ([#] p,d) by A5, FUNCT_2:6; :: thesis: verum

end;

suppose A7: y in {d} ; :: thesis: y in rng ([#] p,d)

dom p = Seg (len p) by FINSEQ_1:def 3;
then A8: not (len p) + 1 in dom p by Lm2;
y = d by A7, TARSKI:def 1;
then y = ([#] p,d) . ((len p) + 1) by A8, Th22;
hence y in rng ([#] p,d) by FUNCT_2:6; :: thesis: verum

end;

end;

end;

hence y in rng ([#] p,d) ; :: thesis: verum

end;

hence rng ([#] p,d) = (rng p) \/ {d} by TARSKI:2; :: thesis: verum