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 & y = p . i ) by FINSEQ_2:11;
( i in NAT & y = ([#] p,d) . i ) by A5, Th22;
hence y in rng ([#] p,d) by FUNCT_2:6; :: thesis: verum

end;

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

dom p = Seg (len p) by FINSEQ_1:def 3;
then ( y = d & not (len p) + 1 in dom p & (len p) + 1 is Element of NAT ) by A6, Lm2, TARSKI:def 1;
then ( y = ([#] p,d) . ((len p) + 1) & (len p) + 1 in NAT ) by 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