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 A3: ( k < G .order() & card (dom (((LexBFS:CSeq G) . k) `1 )) = k ) ; :: thesis: card (dom (((LexBFS:CSeq G) . (k + 1)) `1 )) = k + 1
set CSK = (LexBFS:CSeq G) . k;
set VLK = ((LexBFS:CSeq G) . k) `1 ;
set CK1 = (LexBFS:CSeq G) . (k + 1);
set VK1 = ((LexBFS:CSeq G) . (k + 1)) `1 ;
set w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k);
A5: ((LexBFS:CSeq G) . (k + 1)) `1 = (((LexBFS:CSeq G) . k) `1 ) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k)) .--> ((G .order() ) -' k)) by A3, Th44;
set wf = (LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k)) .--> ((G .order() ) -' k);
( dom ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k)) .--> ((G .order() ) -' k)) = {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k))} & rng ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k)) .--> ((G .order() ) -' k)) = {((G .order() ) -' k)} ) by FUNCOP_1:14, FUNCOP_1:19;
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, Th41, CARD_2:54; :: thesis: verum

end;

(LexBFS:CSeq G) . 0 = LexBFS:Init G by Def33;
then A7: S₁[ 0 ] by CARD_1:47, MCART_1:7, RELAT_1:60;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: 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, A9; :: thesis: verum

end;

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

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

end;

end;

end;

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