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

end;

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;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

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;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