let x, y be Element of NAT ; :: thesis: Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y)
x + y is Element of NAT by ORDINAL1:def 12;
then Nat2BL . (x + y) = (LenBSeq (x + y)) -BinarySequence (x + y) by Def2;
then reconsider adxy = Nat2BL . (x + y) as Tuple of LenBSeq (x + y), BOOLEAN ;
set Nx = Nat2BL . x;
set Ny = Nat2BL . y;
PX2: Nat2BL . x = (LenBSeq x) -BinarySequence x by Def2;
PA3: Nat2BL . y = (LenBSeq y) -BinarySequence y by Def2;
then A3: ( len (Nat2BL . x) <> 0 & len (Nat2BL . y) <> 0 ) by PX2;
B1: Nat2BL . x = (LenBSeq x) -BinarySequence x by Def2;
B2: Nat2BL . y = (LenBSeq y) -BinarySequence y by Def2;
H1: Nat2BL . x in rng Nat2BL by FUNCT_2:4;
PH3: Nat2BL . y in rng Nat2BL by FUNCT_2:4;
PD0: LenMax ((Nat2BL . x),(Nat2BL . y)) = max ((len (Nat2BL . x)),(len (Nat2BL . y))) by PA3, Def15, PX2;
then ( len (Nat2BL . x) <= LenMax ((Nat2BL . x),(Nat2BL . y)) & len (Nat2BL . y) <= LenMax ((Nat2BL . x),(Nat2BL . y)) ) by XXREAL_0:25;
then E0: ( (len (Nat2BL . x)) + 0 <= (LenMax ((Nat2BL . x),(Nat2BL . y))) + 1 & (len (Nat2BL . y)) + 0 <= (LenMax ((Nat2BL . x),(Nat2BL . y))) + 1 ) by XREAL_1:7;

per cases ( ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y)))), ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y)))) are_summable or not ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y)))), ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y)))) are_summable ) ;

suppose C1: ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y)))), ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y)))) are_summable ; :: thesis: Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y)

then C2: (Nat2BL . x) + (Nat2BL . y) = (ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y))))) + (ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y))))) by Def3, A3;
set ENx = ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y))));
set ENy = ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y))));
D1: ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y)))) = (Nat2BL . x) ^ (0* ((LenMax ((Nat2BL . x),(Nat2BL . y))) -' (len (Nat2BL . x)))) by Def20, PD0, XXREAL_0:25;
D2: ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y)))) = (Nat2BL . y) ^ (0* ((LenMax ((Nat2BL . x),(Nat2BL . y))) -' (len (Nat2BL . y)))) by Def20, PD0, XXREAL_0:25;
A4: x = Absval ((LenBSeq x) -BinarySequence x) by LM007
.= Absval (ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y))))) by LM080, B1, D1 ;
y = Absval ((LenBSeq y) -BinarySequence y) by LM007
.= Absval (ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y))))) by LM080, B2, D2 ;
then A6: Nat2BL . (Absval ((ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y))))) + (ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y))))))) = Nat2BL . (x + y) by A4, C1, BINARITH:22;
consider L being Element of NAT such that
H5: (ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y))))) + (ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y))))) = Nat2BL . L by FUNCT_2:113, PH3, C2, LM071, H1;
thus Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y) by A6, C2, LM090, H5; :: thesis: verum

end;

suppose not ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y)))), ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y)))) are_summable ; :: thesis: Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y)

then C2: (Nat2BL . x) + (Nat2BL . y) = (ExtBit ((Nat2BL . x),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))) + (ExtBit ((Nat2BL . y),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))) by Def3, A3;
set ENx = ExtBit ((Nat2BL . x),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1));
set ENy = ExtBit ((Nat2BL . y),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1));
XX1: ExtBit ((Nat2BL . x),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1)) = (ExtBit ((Nat2BL . x),(LenMax ((Nat2BL . x),(Nat2BL . y))))) ^ <*0*> by PD0, LMExtBit1, XXREAL_0:25;
XX2: ExtBit ((Nat2BL . y),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1)) = (ExtBit ((Nat2BL . y),(LenMax ((Nat2BL . x),(Nat2BL . y))))) ^ <*0*> by PD0, LMExtBit1, XXREAL_0:25;
D1: ExtBit ((Nat2BL . x),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1)) = (Nat2BL . x) ^ (0* (((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1) -' (len (Nat2BL . x)))) by Def20, E0;
D2: ExtBit ((Nat2BL . y),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1)) = (Nat2BL . y) ^ (0* (((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1) -' (len (Nat2BL . y)))) by Def20, E0;
A4: x = Absval ((LenBSeq x) -BinarySequence x) by LM007
.= Absval (ExtBit ((Nat2BL . x),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))) by LM080, B1, D1 ;
y = Absval ((LenBSeq y) -BinarySequence y) by LM007
.= Absval (ExtBit ((Nat2BL . y),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))) by LM080, B2, D2 ;
then A6: Nat2BL . (Absval ((ExtBit ((Nat2BL . x),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))) + (ExtBit ((Nat2BL . y),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))))) = Nat2BL . (x + y) by A4, BINARITH:22, XX1, XX2, LMExtBit2;
consider L being Element of NAT such that
H5: (ExtBit ((Nat2BL . x),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))) + (ExtBit ((Nat2BL . y),((LenMax ((Nat2BL . x),(Nat2BL . y))) + 1))) = Nat2BL . L by FUNCT_2:113, PH3, C2, LM071, H1;
thus Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y) by A6, C2, LM090, H5; :: thesis: verum

end;

end;