let n be Nat; :: thesis: for x being Element of NAT
for y being Tuple of n, BOOLEAN st y = Nat2BL . x holds
( n = LenBSeq x & Absval y = x & Nat2BL . (Absval y) = y )
let x be Element of NAT ; :: thesis: for y being Tuple of n, BOOLEAN st y = Nat2BL . x holds
( n = LenBSeq x & Absval y = x & Nat2BL . (Absval y) = y )
let y be Tuple of n, BOOLEAN ; :: thesis: ( y = Nat2BL . x implies ( n = LenBSeq x & Absval y = x & Nat2BL . (Absval y) = y ) )
assume AS: y = Nat2BL . x ; :: thesis: ( n = LenBSeq x & Absval y = x & Nat2BL . (Absval y) = y )
A1: Nat2BL . x = (LenBSeq x) -BinarySequence x by Def2;
A3: x < 2 to_power (LenBSeq x) by LM006;
len y = LenBSeq x by CARD_1:def 7, AS, A1;
hence n = LenBSeq x by CARD_1:def 7; :: thesis: ( Absval y = x & Nat2BL . (Absval y) = y )
hence ( Absval y = x & Nat2BL . (Absval y) = y ) by A3, BINARI_3:35, A1, AS; :: thesis: verum