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 :: thesis: for y being object holds
( ( y in rng ([#] (p,d)) implies y in (rng p) \/ {d} ) & ( y in (rng p) \/ {d} implies y in rng ([#] (p,d)) ) )

let y be object ; :: 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 object such that
A1: x in dom ([#] (p,d)) and
A2: y = ([#] (p,d)) . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A1;

now :: thesis: ( ( i in dom p & y in rng p ) or ( not i in dom p & y in {d} ) )

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, Th20;
hence y in rng p by A3, FUNCT_1:def 3; :: thesis: verum

end;

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

then y = d by A2, Th20;
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 :: thesis: y in rng ([#] (p,d))

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:10;
y = ([#] (p,d)) . i by A5, A6, Th20;
hence y in rng ([#] (p,d)) by A5, FUNCT_2:4; :: 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, Th20;
hence y in rng ([#] (p,d)) by FUNCT_2:4; :: 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