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

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

then A2: card C1 is even by Th63;
card C2 is even by A1, Th63;
then card (C1 + C2) is even by A2, Th7;
hence C1 + C2 is Cycle of k,G by A1, Th63; :: thesis: verum

end;

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

then consider k9 being Nat such that
A3: k = k9 + 1 ;
reconsider k9 = k9 as Element of NAT by ORDINAL1:def 12;
reconsider C1 = C1, C2 = C2 as Cycle of k9 + 1,G by A3;
A4: del C1 = 0_ (k9,G) ;
del C2 = 0_ (k9,G) ;
then del (C1 + C2) = (0_ (k9,G)) + (0_ (k9,G)) by A4, Th58
.= 0_ (k9,G) ;
hence + is Cycle of k,G by A3, Th61; :: thesis: verum

end;

end;