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;