let n be non zero Nat; :: thesis: for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN
for i being Nat st i in Seg n holds
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
let z1, z2 be Tuple of n, BOOLEAN ; :: thesis: for d1, d2 being Element of BOOLEAN
for i being Nat st i in Seg n holds
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
let d1, d2 be Element of BOOLEAN ; :: thesis: for i being Nat st i in Seg n holds
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
defpred S₁[ Nat] means ( $1 in Seg n implies (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. $1 = (carry (z1,z2)) /. $1 );
let i be Nat; :: thesis: ( i in Seg n implies (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i )
A1: for i being non zero Nat st S₁[i] holds
S₁[i + 1]

proof

let i be non zero Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: S₁[i] ; :: thesis: S₁[i + 1]
assume i + 1 in Seg n ; :: thesis: (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (i + 1) = (carry (z1,z2)) /. (i + 1)
then ( i + 1 > i & i + 1 <= n ) by FINSEQ_1:1, XREAL_1:29;
then A3: i < n by XXREAL_0:2;
n <= n + 1 by NAT_1:11;
then A4: i < n + 1 by A3, XXREAL_0:2;
A5: 1 <= i by NAT_1:14;
then i in Seg n by A3;
then ( (z1 ^ <*d1*>) /. i = z1 /. i & (z2 ^ <*d2*>) /. i = z2 /. i ) by Th1;
hence (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (i + 1) = (((z1 /. i) '&' (z2 /. i)) 'or' ((z1 /. i) '&' ((carry (z1,z2)) /. i))) 'or' ((z2 /. i) '&' ((carry (z1,z2)) /. i)) by A2, A5, A3, A4, Def2
.= (carry (z1,z2)) /. (i + 1) by A5, A3, Def2 ;
:: thesis: verum

end;

A6: S₁[1]

proof

assume 1 in Seg n ; :: thesis: (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. 1 = (carry (z1,z2)) /. 1
thus (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. 1 = FALSE by Def2
.= (carry (z1,z2)) /. 1 by Def2 ; :: thesis: verum

end;

A7: for i being non zero Nat holds S₁[i] from NAT_1:sch 10(A6, A1);
assume A8: i in Seg n ; :: thesis: (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
then not i is zero by FINSEQ_1:1;
hence (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i by A8, A7; :: thesis: verum