thus ( len x <= K implies x ^ (0* (K -' (len x))) is Tuple of K, BOOLEAN ) :: thesis: ( not len x <= K implies x | K is Tuple of K, BOOLEAN )
proof
assume len x <= K ; :: thesis: x ^ (0* (K -' (len x))) is Tuple of K, BOOLEAN
then A2: K -' (len x) = K - (len x) by XREAL_0:def 2, XREAL_1:48;
0* (K -' (len x)) in BOOLEAN * by BINARI_3:4;
then reconsider z = 0* (K -' (len x)) as Tuple of K -' (len x), BOOLEAN by FINSEQ_1:def 11;
x is Element of (len x) -tuples_on BOOLEAN by FINSEQ_2:92;
then reconsider y = x as Tuple of len x, BOOLEAN ;
y ^ z is Tuple of K, BOOLEAN by A2;
hence x ^ (0* (K -' (len x))) is Tuple of K, BOOLEAN ; :: thesis: verum
end;
thus ( not len x <= K implies x | K is Tuple of K, BOOLEAN ) :: thesis: verum
proof
assume not len x <= K ; :: thesis: x | K is Tuple of K, BOOLEAN
then A1: len (x | K) = K by FINSEQ_1:59;
x | K is Element of (len (x | K)) -tuples_on BOOLEAN by FINSEQ_2:92;
hence x | K is Tuple of K, BOOLEAN by A1; :: thesis: verum
end;