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;