let n be Nat; :: thesis: for z, z1 being Element of BOOLEAN * st z = <*> BOOLEAN & z1 = 0* n holds
Class (EqBL2Nat,z) = Class (EqBL2Nat,z1)
let z, z1 be Element of BOOLEAN * ; :: thesis: ( z = <*> BOOLEAN & z1 = 0* n implies Class (EqBL2Nat,z) = Class (EqBL2Nat,z1) )
assume AS: ( z = <*> BOOLEAN & z1 = 0* n ) ; :: thesis: Class (EqBL2Nat,z) = Class (EqBL2Nat,z1)
then P1: len z = 0 ;
P2: BL2Nat . z = ExAbsval z by Def110
.= 0 by D100, P1 ;
P3: BL2Nat . z1 = ExAbsval z1 by Def110;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: Class (EqBL2Nat,z) = Class (EqBL2Nat,z1)
hence Class (EqBL2Nat,z) = Class (EqBL2Nat,z1) by AS; :: thesis: verum
end;
suppose nz: n <> 0 ; :: thesis: Class (EqBL2Nat,z) = Class (EqBL2Nat,z1)
consider n1 being Nat, y being Tuple of n1, BOOLEAN such that
C2: ( y = z1 & ExAbsval z1 = Absval y ) by Def100;
n1 = len y by CARD_1:def 7
.= n by CARD_1:def 7, AS, C2 ;
then BL2Nat . z1 = 0 by nz, C2, P3, AS, BINARI_3:6;
then [z,z1] in EqBL2Nat by P2, Def300;
hence Class (EqBL2Nat,z) = Class (EqBL2Nat,z1) by EQREL_1:35; :: thesis: verum
end;
end;