let z1, z2 be Tuple of n, BOOLEAN ; :: thesis: ( z1 /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
z1 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z1 /. i))) 'or' ((y /. i) '&' (z1 /. i)) ) & z2 /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
z2 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z2 /. i))) 'or' ((y /. i) '&' (z2 /. i)) ) implies z1 = z2 )
assume that
A16: z1 /. 1 = FALSE and
A17: for i being Nat st 1 <= i & i < n holds
z1 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z1 /. i))) 'or' ((y /. i) '&' (z1 /. i)) and
A18: z2 /. 1 = FALSE and
A19: for i being Nat st 1 <= i & i < n holds
z2 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z2 /. i))) 'or' ((y /. i) '&' (z2 /. i)) ; :: thesis: z1 = z2
A20: len z2 = n by CARD_1:def 7;
A21: len z1 = n by CARD_1:def 7;
then A22: dom z1 = Seg n by FINSEQ_1:def 3;

now :: thesis: for j being Nat st j in dom z1 holds
z1 . j = z2 . j

defpred S₁[ Nat] means ( $1 in Seg n implies z1 /. $1 = z2 /. $1 );
A23: ( dom z1 = Seg n & dom z2 = Seg n ) by A21, A20, FINSEQ_1:def 3;

A24: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A25: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume A26: k + 1 in Seg n ; :: thesis: z1 /. (k + 1) = z2 /. (k + 1)

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: z1 /. (k + 1) = z2 /. (k + 1)

hence z1 /. (k + 1) = z2 /. (k + 1) by A16, A18; :: thesis: verum

end;

suppose A27: k <> 0 ; :: thesis: z1 /. (k + 1) = z2 /. (k + 1)

( k + 1 <= n & k < k + 1 ) by A26, FINSEQ_1:1, XREAL_1:29;
then A28: k < n by XXREAL_0:2;
A29: k >= 0 + 1 by A27, NAT_1:13;
hence z1 /. (k + 1) = (((x /. k) '&' (y /. k)) 'or' ((x /. k) '&' (z1 /. k))) 'or' ((y /. k) '&' (z1 /. k)) by A17, A28
.= z2 /. (k + 1) by A19, A25, A29, A28 ;
:: thesis: verum

end;

end;

end;

end;

A30: S₁[ 0 ] by FINSEQ_1:1;
A31: for k being Nat holds S₁[k] from NAT_1:sch 2(A30, A24);
let j be Nat; :: thesis: ( j in dom z1 implies z1 . j = z2 . j )
assume A32: j in dom z1 ; :: thesis: z1 . j = z2 . j
thus z1 . j = z1 /. j by A32, PARTFUN1:def 6
.= z2 /. j by A22, A32, A31
.= z2 . j by A32, A23, PARTFUN1:def 6 ; :: thesis: verum

end;

hence z1 = z2 by A21, A20, FINSEQ_2:9; :: thesis: verum