let z1 be Tuple of 1,BOOLEAN ; :: thesis: ( z1 = <*FALSE *> or z1 = <*TRUE *> )
consider B being Element of BOOLEAN such that
A1: z1 = <*B*> by FINSEQ_2:117;

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:25; :: thesis: verum

end;

suppose z1 /. 1 = TRUE ; :: thesis: ( z1 = <*FALSE *> or z1 = <*TRUE *> )

hence ( z1 = <*FALSE *> or z1 = <*TRUE *> ) by A1, FINSEQ_4:25; :: thesis: verum

end;

end;