defpred S_{1}[ non zero Nat] means for F1, F2 being Tuple of $1, BOOLEAN st Absval F1 = Absval F2 holds

F1 = F2;

A1: for k being non zero Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[1]
_{1}[n]
from NAT_1:sch 10(A12, A1); :: thesis: verum

F1 = F2;

A1: for k being non zero Nat st S

S

proof

A12:
S
let k be non zero Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: for F1, F2 being Tuple of k, BOOLEAN st Absval F1 = Absval F2 holds

F1 = F2 ; :: thesis: S_{1}[k + 1]

let F1, F2 be Tuple of k + 1, BOOLEAN ; :: thesis: ( Absval F1 = Absval F2 implies F1 = F2 )

consider T1 being Element of k -tuples_on BOOLEAN, d1 being Element of BOOLEAN such that

A3: F1 = T1 ^ <*d1*> by FINSEQ_2:117;

assume A4: Absval F1 = Absval F2 ; :: thesis: F1 = F2

consider T2 being Element of k -tuples_on BOOLEAN, d2 being Element of BOOLEAN such that

A5: F2 = T2 ^ <*d2*> by FINSEQ_2:117;

A6: (Absval T1) + (IFEQ (d1,FALSE,0,(2 to_power k))) = Absval F1 by A3, BINARITH:20

.= (Absval T2) + (IFEQ (d2,FALSE,0,(2 to_power k))) by A5, A4, BINARITH:20 ;

d1 = d2

end;assume A2: for F1, F2 being Tuple of k, BOOLEAN st Absval F1 = Absval F2 holds

F1 = F2 ; :: thesis: S

let F1, F2 be Tuple of k + 1, BOOLEAN ; :: thesis: ( Absval F1 = Absval F2 implies F1 = F2 )

consider T1 being Element of k -tuples_on BOOLEAN, d1 being Element of BOOLEAN such that

A3: F1 = T1 ^ <*d1*> by FINSEQ_2:117;

assume A4: Absval F1 = Absval F2 ; :: thesis: F1 = F2

consider T2 being Element of k -tuples_on BOOLEAN, d2 being Element of BOOLEAN such that

A5: F2 = T2 ^ <*d2*> by FINSEQ_2:117;

A6: (Absval T1) + (IFEQ (d1,FALSE,0,(2 to_power k))) = Absval F1 by A3, BINARITH:20

.= (Absval T2) + (IFEQ (d2,FALSE,0,(2 to_power k))) by A5, A4, BINARITH:20 ;

d1 = d2

proof

hence
F1 = F2
by A2, A3, A5, A6, XCMPLX_1:2; :: thesis: verum
assume A7:
d1 <> d2
; :: thesis: contradiction

end;per cases
( d1 = FALSE or d1 = TRUE )
by XBOOLEAN:def 3;

end;

proof

thus
for n being non zero Nat holds S
let F1, F2 be Tuple of 1, BOOLEAN ; :: thesis: ( Absval F1 = Absval F2 implies F1 = F2 )

consider d1 being Element of BOOLEAN such that

A13: F1 = <*d1*> by FINSEQ_2:97;

assume A14: Absval F1 = Absval F2 ; :: thesis: F1 = F2

assume A15: F1 <> F2 ; :: thesis: contradiction

consider d2 being Element of BOOLEAN such that

A16: F2 = <*d2*> by FINSEQ_2:97;

end;consider d1 being Element of BOOLEAN such that

A13: F1 = <*d1*> by FINSEQ_2:97;

assume A14: Absval F1 = Absval F2 ; :: thesis: F1 = F2

assume A15: F1 <> F2 ; :: thesis: contradiction

consider d2 being Element of BOOLEAN such that

A16: F2 = <*d2*> by FINSEQ_2:97;

per cases
( d1 = FALSE or d1 = TRUE )
by XBOOLEAN:def 3;

end;

suppose A17:
d1 = FALSE
; :: thesis: contradiction

then A18:
Absval F1 = 0
by A13, BINARITH:15;

d2 = TRUE by A13, A16, A15, A17, XBOOLEAN:def 3;

hence contradiction by A16, A14, A18, BINARITH:16; :: thesis: verum

end;d2 = TRUE by A13, A16, A15, A17, XBOOLEAN:def 3;

hence contradiction by A16, A14, A18, BINARITH:16; :: thesis: verum

suppose A19:
d1 = TRUE
; :: thesis: contradiction

then A20:
Absval F1 = 1
by A13, BINARITH:16;

d2 = FALSE by A13, A16, A15, A19, XBOOLEAN:def 3;

hence contradiction by A16, A14, A20, BINARITH:15; :: thesis: verum

end;d2 = FALSE by A13, A16, A15, A19, XBOOLEAN:def 3;

hence contradiction by A16, A14, A20, BINARITH:15; :: thesis: verum