defpred S₁[ non empty Nat] means for F1, F2 being Tuple of $1,BOOLEAN st Absval F1 = Absval F2 holds
F1 = F2;
A1: 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
A2: F1 = <*d1*> by FINSEQ_2:117;
consider d2 being Element of BOOLEAN such that
A3: F2 = <*d2*> by FINSEQ_2:117;
assume A4: Absval F1 = Absval F2 ; :: thesis: F1 = F2
assume A5: F1 <> F2 ; :: thesis: contradiction

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

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

then d2 = TRUE by A2, A3, A5, XBOOLEAN:def 3;
then ( Absval F1 = 0 & Absval F2 = 1 ) by A2, A3, A6, BINARITH:41, BINARITH:42;
hence contradiction by A4; :: thesis: verum

end;

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

then d2 = FALSE by A2, A3, A5, XBOOLEAN:def 3;
then ( Absval F1 = 1 & Absval F2 = 0 ) by A2, A3, A7, BINARITH:41, BINARITH:42;
hence contradiction by A4; :: thesis: verum

end;

end;

end;

A8: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: 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 Tuple of k,BOOLEAN , d1 being Element of BOOLEAN such that
A10: F1 = T1 ^ <*d1*> by FINSEQ_2:137;
consider T2 being Tuple of k,BOOLEAN , d2 being Element of BOOLEAN such that
A11: F2 = T2 ^ <*d2*> by FINSEQ_2:137;
assume A12: Absval F1 = Absval F2 ; :: thesis: F1 = F2
A13: (Absval T1) + (IFEQ d1,FALSE ,0 ,(2 to_power k)) = Absval F1 by A10, BINARITH:46
.= (Absval T2) + (IFEQ d2,FALSE ,0 ,(2 to_power k)) by A11, A12, BINARITH:46 ;
d1 = d2

proof

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

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

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

then A16: IFEQ d2,FALSE ,0 ,(2 to_power k) = 2 to_power k by A14, FUNCOP_1:def 8;
IFEQ d1,FALSE ,0 ,(2 to_power k) = 0 by A15, FUNCOP_1:def 8;
hence contradiction by A13, A16, Th1, NAT_1:11; :: thesis: verum

end;

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

then d2 = FALSE by A14, XBOOLEAN:def 3;
then A18: 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 A17, FUNCOP_1:def 8;
hence contradiction by A13, A18, Th1, NAT_1:11; :: thesis: verum

end;

end;

end;

hence F1 = F2 by A9, A10, A11, A13, XCMPLX_1:2; :: thesis: verum

end;

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