defpred S₁[ 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₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for F1, F2 being Tuple of k, BOOLEAN st Absval F1 = Absval F2 holds
F1 = F2 ; :: thesis: S₁[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

proof

assume A7: d1 <> d2 ; :: thesis: contradiction

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

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

then A9: IFEQ (d1,FALSE,0,(2 to_power k)) = 0 by FUNCOP_1:def 8;
IFEQ (d2,FALSE,0,(2 to_power k)) = 2 to_power k by A7, A8, FUNCOP_1:def 8;
hence contradiction by A6, A9, Th1, NAT_1:11; :: thesis: verum

end;

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

then d2 = FALSE by A7, XBOOLEAN:def 3;
then A11: IFEQ (d2,FALSE,0,(2 to_power k)) = 0 by FUNCOP_1:def 8;
IFEQ (d1,FALSE,0,(2 to_power k)) = 2 to_power k by A10, FUNCOP_1:def 8;
hence contradiction by A6, A11, Th1, NAT_1:11; :: thesis: verum

end;

end;

end;

hence F1 = F2 by A2, A3, A5, A6, XCMPLX_1:2; :: thesis: verum

end;

A12: S₁[1]

proof

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;

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

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;

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;

end;

end;

thus for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A12, A1); :: thesis: verum