let p be FinSequence; for x being object
for D being non empty set st x in rng p & p is FinSequence of D holds
p |-- x is FinSequence of D
let x be object ; for D being non empty set st x in rng p & p is FinSequence of D holds
p |-- x is FinSequence of D
let D be non empty set ; ( x in rng p & p is FinSequence of D implies p |-- x is FinSequence of D )
assume that
A1:
x in rng p
and
A2:
p is FinSequence of D
; p |-- x is FinSequence of D
rng (p |-- x) c= D
proof
A3:
len (p |-- x) = (len p) - (x .. p)
by A1, Def6;
let y be
object ;
TARSKI:def 3 ( not y in rng (p |-- x) or y in D )
assume
y in rng (p |-- x)
;
y in D
then consider z being
object such that A4:
z in dom (p |-- x)
and A5:
(p |-- x) . z = y
by FUNCT_1:def 3;
reconsider z =
z as
Element of
NAT by A4;
dom (p |-- x) = Seg (len (p |-- x))
by FINSEQ_1:def 3;
then
z <= len (p |-- x)
by A4, FINSEQ_1:1;
then A6:
z + (x .. p) <= len p
by A3, XREAL_1:19;
1
<= z + (x .. p)
by A1, Th21, NAT_1:12;
then
z + (x .. p) in Seg (len p)
by A6;
then A7:
z + (x .. p) in dom p
by FINSEQ_1:def 3;
y = p . (z + (x .. p))
by A1, A4, A5, Def6;
then A8:
y in rng p
by A7, FUNCT_1:def 3;
rng p c= D
by A2, FINSEQ_1:def 4;
hence
y in D
by A8;
verum
end;
hence
p |-- x is FinSequence of D
by FINSEQ_1:def 4; verum