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 A2: card C1 is even by Th68;
card C2 is even by A1, Th68;
then card (C1 + C2) is even by A2, 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
A3: 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 A3;
A4: del C1 = 0_ k',G ;
del C2 = 0_ k',G ;
then del (C1 + C2) = (0_ k',G) + (0_ k',G) by A4, Th63
.= 0_ k',G ;
hence + is Cycle of k,G by A3, Th66; :: thesis: verum

end;

end;