let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN st x,y are_summable & ( x . (len x) = 1 or y . (len y) = 1 ) holds
(x + y) . (len (x + y)) = 1
let x, y be Tuple of K, BOOLEAN ; :: thesis: ( x,y are_summable & ( x . (len x) = 1 or y . (len y) = 1 ) implies (x + y) . (len (x + y)) = 1 )
assume AS: ( x,y are_summable & ( x . (len x) = 1 or y . (len y) = 1 ) ) ; :: thesis: (x + y) . (len (x + y)) = 1
x + y = y + x by LMExtBit500;
hence (x + y) . (len (x + y)) = 1 by LMExtBit60, LMExtBit61, AS; :: thesis: verum