let n be Nat; for y being Tuple of n, BOOLEAN st y = 0* n holds
'not' y = n |-> 1
let y be Tuple of n, BOOLEAN ; ( y = 0* n implies 'not' y = n |-> 1 )
assume A1:
y = 0* n
; 'not' y = n |-> 1
A2:
now for i being Nat st 1 <= i & i <= len ('not' y) holds
('not' y) . i = (n |-> 1) . iA3:
len y = n
by CARD_1:def 7;
let i be
Nat;
( 1 <= i & i <= len ('not' y) implies ('not' y) . i = (n |-> 1) . i )assume that A4:
1
<= i
and A5:
i <= len ('not' y)
;
('not' y) . i = (n |-> 1) . iA6:
len ('not' y) = n
by CARD_1:def 7;
then A7:
i in Seg n
by A4, A5, FINSEQ_1:1;
then A8:
y . i = FALSE
by A1, FUNCOP_1:7;
thus ('not' y) . i =
('not' y) /. i
by A4, A5, FINSEQ_4:15
.=
'not' (y /. i)
by A7, BINARITH:def 1
.=
'not' FALSE
by A4, A5, A6, A3, A8, FINSEQ_4:15
.=
(n |-> 1) . i
by A7, FUNCOP_1:7
;
verum end;
len ('not' y) =
n
by CARD_1:def 7
.=
len (n |-> 1)
by CARD_1:def 7
;
hence
'not' y = n |-> 1
by A2, FINSEQ_1:14; verum