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 S1[ 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 S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A25: S1[k] ; :: thesis: S1[k + 1]
thus S1[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: S1[ 0 ] by FINSEQ_1:1;
A31: for k being Nat holds S1[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