let x be Element of NAT ; :: thesis: for y being Tuple of LenBSeq x, BOOLEAN st Nat2BL . x = y holds
Absval y = x
let y be Tuple of LenBSeq x, BOOLEAN ; :: thesis: ( Nat2BL . x = y implies Absval y = x )
assume AS: Nat2BL . x = y ; :: thesis: Absval y = x
Nat2BL . x = (LenBSeq x) -BinarySequence x by Def2;
hence Absval y = x by AS, LM007; :: thesis: verum