let G be _finite _Graph; :: thesis: for n being Nat st n <= G .order() holds
card (dom (((LexBFS:CSeq G) . n) `1)) = n
let n be Nat; :: thesis: ( n <= G .order() implies card (dom (((LexBFS:CSeq G) . n) `1)) = n )
assume A1: n <= G .order() ; :: thesis: card (dom (((LexBFS:CSeq G) . n) `1)) = n
set CS = LexBFS:CSeq G;
defpred S<sub>1</sub>[ Nat] means ( $1 <= G .order() implies card (dom (((LexBFS:CSeq G) . $1) `1)) = $1 );
A2: for k being Nat st k < G .order() & card (dom (((LexBFS:CSeq G) . k) `1)) = k holds
card (dom (((LexBFS:CSeq G) . (k + 1)) `1)) = k + 1

proof

let k be Nat; :: thesis: ( k < G .order() & card (dom (((LexBFS:CSeq G) . k) `1)) = k implies card (dom (((LexBFS:CSeq G) . (k + 1)) `1)) = k + 1 )
assume that
A3: k < G .order() and
A4: card (dom (((LexBFS:CSeq G) . k) `1)) = k ; :: thesis: card (dom (((LexBFS:CSeq G) . (k + 1)) `1)) = k + 1
set CK1 = (LexBFS:CSeq G) . (k + 1);
set CSK = (LexBFS:CSeq G) . k;
set VLK = ((LexBFS:CSeq G) . k) `1 ;
set VK1 = ((LexBFS:CSeq G) . (k + 1)) `1 ;
set w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k);
set wf = (LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k)) .--> ((G .order()) -' k);
A5: dom ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k)) .--> ((G .order()) -' k)) = {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k))} ;
((LexBFS:CSeq G) . (k + 1)) `1 = (((LexBFS:CSeq G) . k) `1) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k)) .--> ((G .order()) -' k)) by A3, A4, Th31;
then dom (((LexBFS:CSeq G) . (k + 1)) `1) = (dom (((LexBFS:CSeq G) . k) `1)) \/ {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k))} by A5, FUNCT_4:def 1;
hence card (dom (((LexBFS:CSeq G) . (k + 1)) `1)) = k + 1 by A3, A4, Th30, CARD_2:41; :: thesis: verum

end;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( k < G .order() or k >= G .order() ) ;

suppose k < G .order() ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by A2, A7; :: thesis: verum

end;

suppose k >= G .order() ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by NAT_1:13; :: thesis: verum

end;

end;

end;

(LexBFS:CSeq G) . 0 = LexBFS:Init G by Def16;
then A8: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A6);
hence card (dom (((LexBFS:CSeq G) . n) `1)) = n by A1; :: thesis: verum