let z1 be Tuple of 1, BOOLEAN ; :: thesis: ( z1 = <*FALSE*> or z1 = <*TRUE*> )
A1: ex B being Element of BOOLEAN st z1 = <*B*> by FINSEQ_2:97;
per cases ( z1 /. 1 = FALSE or z1 /. 1 = TRUE ) by XBOOLEAN:def 3;
suppose z1 /. 1 = FALSE ; :: thesis: ( z1 = <*FALSE*> or z1 = <*TRUE*> )
hence ( z1 = <*FALSE*> or z1 = <*TRUE*> ) by A1, FINSEQ_4:16; :: thesis: verum
end;
suppose z1 /. 1 = TRUE ; :: thesis: ( z1 = <*FALSE*> or z1 = <*TRUE*> )
hence ( z1 = <*FALSE*> or z1 = <*TRUE*> ) by A1, FINSEQ_4:16; :: thesis: verum
end;
end;