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}

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)) ) )

hence
rng ([#] (p,d)) = (rng p) \/ {d}
by TARSKI:2; :: thesis: verum( ( 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)) )

end;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 A4:
y in (rng p) \/ {d}
; :: thesis: y in rng ([#] (p,d))
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;

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

end;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;

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

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

hence
y in rng ([#] (p,d))
; :: thesis: verumper cases
( y in rng p or y in {d} )
by A4, XBOOLE_0:def 3;

end;