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 ) ;
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 ;
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 ; :: 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 ;
then y = ([#] (p,d)) . ((len p) + 1) by ;
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