let X be non empty set ; :: thesis: for f being FinSequence of X holds PairF f is FinSequence of the carrier' of (PGraph X)
let f be FinSequence of X; :: thesis: PairF f is FinSequence of the carrier' of (PGraph X)
rng (PairF f) c= [:X,X:]
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng (PairF f) or y in [:X,X:] )
assume
y in rng (PairF f)
;
:: thesis: y in [:X,X:]
then consider x being
set such that A1:
(
x in dom (PairF f) &
y = (PairF f) . x )
by FUNCT_1:def 5;
A2:
x in Seg (len (PairF f))
by A1, FINSEQ_1:def 3;
reconsider n =
x as
Element of
NAT by A1;
A3:
( 1
<= n &
n <= len (PairF f) )
by A2, FINSEQ_1:3;
A4:
len (PairF f) = (len f) -' 1
by Def2;
then
1
<= (len f) -' 1
by A3, XXREAL_0:2;
then A5:
(len f) -' 1
= (len f) - 1
by NAT_D:39;
(len f) -' 1
< ((len f) -' 1) + 1
by NAT_1:13;
then A6:
n < len f
by A3, A4, A5, XXREAL_0:2;
then A7:
(PairF f) . n = [(f . n),(f . (n + 1))]
by A3, Def2;
n in dom f
by A3, A6, FINSEQ_3:27;
then A8:
f . n in rng f
by FUNCT_1:def 5;
A9:
1
< n + 1
by A3, NAT_1:13;
n + 1
<= len f
by A6, NAT_1:13;
then
n + 1
in dom f
by A9, FINSEQ_3:27;
then
f . (n + 1) in rng f
by FUNCT_1:def 5;
hence
y in [:X,X:]
by A1, A7, A8, ZFMISC_1:def 2;
:: thesis: verum
end;
hence
PairF f is FinSequence of the carrier' of (PGraph X)
by FINSEQ_1:def 4; :: thesis: verum