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