let A, Z be Element of Class EqBL2Nat; :: thesis: for n being Nat
for z being Element of BOOLEAN * st Z = Class (EqBL2Nat,z) & z = 0* n holds
( A + Z = A & Z + A = A )
let n be Nat; :: thesis: for z being Element of BOOLEAN * st Z = Class (EqBL2Nat,z) & z = 0* n holds
( A + Z = A & Z + A = A )
let z be Element of BOOLEAN * ; :: thesis: ( Z = Class (EqBL2Nat,z) & z = 0* n implies ( A + Z = A & Z + A = A ) )
assume AS: ( Z = Class (EqBL2Nat,z) & z = 0* n ) ; :: thesis: ( A + Z = A & Z + A = A )
reconsider zempty = <*> BOOLEAN as Element of BOOLEAN * by FINSEQ_1:def 11;
Z = Class (EqBL2Nat,zempty) by AS, LM930;
then P3: zempty in Z by EQREL_1:20;
P4: len zempty = 0 ;
P0: A in Class EqBL2Nat ;
consider x being object such that
Q1: ( x in BOOLEAN * & A = Class (EqBL2Nat,x) ) by P0, EQREL_1:def 3;
reconsider x = x as Element of BOOLEAN * by Q1;
x in A by Q1, EQREL_1:20;
hence A + Z = Class (EqBL2Nat,(x + zempty)) by P3, LM800
.= A by Q1, P4, Def3 ;
:: thesis: Z + A = A
hence Z + A = A by LM910; :: thesis: verum