per cases ( k = 0 or ex k' being Nat st k = k' + 1 ) by NAT_1:6;

suppose A1: k = 0 ; :: thesis: + is Cycle of k,G

then ( card C1 is even & card C2 is even ) by Th68;
then card (C1 + C2) is even by Th9;
hence C1 + C2 is Cycle of k,G by A1, Th68; :: thesis: verum

end;

suppose ex k' being Nat st k = k' + 1 ; :: thesis: + is Cycle of k,G

then consider k' being Nat such that
A2: k = k' + 1 ;
reconsider k' = k' as Element of NAT by ORDINAL1:def 13;
reconsider C1 = C1, C2 = C2 as Cycle of k' + 1,G by A2;
( del C1 = 0_ k',G & del C2 = 0_ k',G ) ;
then del (C1 + C2) = (0_ k',G) + (0_ k',G) by Th63
.= 0_ k',G ;
hence + is Cycle of k,G by A2, Th66; :: thesis: verum

end;

end;