proof

let c₁ be set ;
assume E3: c₁ is (B2) ;
let c₂ be set ;
let c₃ be finite Subset-Family of c₂;
assume that
E4: c₂ in c₁ and
E5: c₃ c= c₁ ;
defpred S₁[ set ] means for b₁ being Subset-Family of c₂ holds
( b₁ = a₁ implies Intersect b₁ in c₁ );
E6: c₃ is finite ;
E7: S₁[ {} ] by E4, SETFAM_1:def 10;

E8: now

let c₄, c₅ be set ;
assume that
E9: c₄ in c₃ and
E10: c₅ c= c₃ and
E11: S₁[c₅] ;
thus S₁[c₅ \/ {c₄}]

proof

let c₆ be Subset-Family of c₂;
assume E12: c₆ = c₅ \/ {c₄} ;
reconsider c₇ = c₄ as Subset of c₂ by E9;
c₅ c= bool c₂ by E10, XBOOLE_1:1;
then reconsider c₈ = c₅ as Subset-Family of c₂ ;
{c₄} c= bool c₂ by E9, ZFMISC_1:37;
then reconsider c₉ = {c₄} as Subset-Family of c₂ ;
E13: Intersect c₈ in c₁ by E11;
Intersect (c₈ \/ c₉) = (Intersect c₈) /\ (Intersect c₉) by MSSUBFAM:8
.= (Intersect c₈) /\ c₇ by MSSUBFAM:9 ;
hence Intersect c₆ in c₁ by E3, E5, E9, E12, E13, FINSUB_1:def 2;

end;

S₁[c₃] from FINSET_1:sch 2(E6, E7, E8);
hence Intersect c₃ in c₁ ;

end;

registration

cluster non empty reflexive antisymmetric transitive set ;
existence

proof

set c₁ = {[{} ,{} ]};
reconsider c₂ = {[{} ,{} ]} as Relation by RELAT_1:4;
E3: field c₂ = {{} ,{} } by RELAT_1:32
.= {{} } by ENUMSET1:69 ;
take c₂ ;
thus c₂ is reflexive

proof

let c₃ be set ; :: according to RELAT_2:def 1,RELAT_2:def 9
assume c₃ in field c₂ ;
then c₃ = {} by E3, TARSKI:def 1;
hence [c₃,c₃] in c₂ by TARSKI:def 1;

end;

thus c₂ is antisymmetric

proof

let c₃, c₄ be set ; :: according to RELAT_2:def 4,RELAT_2:def 12
assume ( c₃ in field c₂ & c₄ in field c₂ & [c₃,c₄] in c₂ & [c₄,c₃] in c₂ ) ;
then ( c₃ = {} & c₄ = {} ) by E3, TARSKI:def 1;
hence c₃ = c₄ ;

end;

thus c₂ is (F2)

proof

let c₃, c₄, c₅ be set ; :: according to RELAT_2:def 8,RELAT_2:def 16
assume ( c₃ in field c₂ & c₄ in field c₂ & c₅ in field c₂ & [c₃,c₄] in c₂ & [c₄,c₅] in c₂ ) ;
then ( c₃ = {} & c₅ = {} ) by E3, TARSKI:def 1;
hence [c₃,c₅] in c₂ by TARSKI:def 1;

end;

thus c₂ is (C1) ;

end;

proof

let c₁ be non empty antisymmetric transitive Relation;
let c₂ be finite Subset of (field c₁);
assume E4: c₂ <> {} ;
reconsider c₃ = c₁ as Relation of field c₁ by POLYNOM1:4;
set c₄ = RelStr(# (field c₁),c₃ #);
set c₅ = the carrier of RelStr(# (field c₁),c₃ #);
set c₆ = the InternalRel of RelStr(# (field c₁),c₃ #);
E5: the carrier of RelStr(# (field c₁),c₃ #) is (C1) by E4, XBOOLE_1:3;
E6: c₁ is_antisymmetric_in field c₁ by RELAT_2:def 12;
E7: RelStr(# (field c₁),c₃ #) is antisymmetric

proof

let c₇, c₈ be Element of RelStr(# (field c₁),c₃ #); :: according to YELLOW_0:def 3
assume ( c₇ <= c₈ & c₈ <= c₇ ) ;
then ( [c₇,c₈] in the InternalRel of RelStr(# (field c₁),c₃ #) & [c₈,c₇] in the InternalRel of RelStr(# (field c₁),c₃ #) ) by ORDERS_2:def 9;
hence c₇ = c₈ by E5, E6, RELAT_2:def 4;

end;

E8: c₁ is_transitive_in field c₁ by RELAT_2:def 16;
RelStr(# (field c₁),c₃ #) is transitive

proof

let c₇, c₈, c₉ be Element of RelStr(# (field c₁),c₃ #); :: according to YELLOW_0:def 2
assume ( c₇ <= c₈ & c₈ <= c₉ ) ;
then ( [c₇,c₈] in the InternalRel of RelStr(# (field c₁),c₃ #) & [c₈,c₉] in the InternalRel of RelStr(# (field c₁),c₃ #) ) by ORDERS_2:def 9;
then [c₇,c₉] in the InternalRel of RelStr(# (field c₁),c₃ #) by E5, E8, RELAT_2:def 8;
hence c₇ <= c₉ by ORDERS_2:def 9;

end;

then reconsider c₇ = RelStr(# (field c₁),c₃ #) as non empty transitive antisymmetric RelStr by E5, E7, STRUCT_0:def 1;
reconsider c₈ = c₂ as finite Subset of the carrier of RelStr(# (field c₁),c₃ #) ;
consider c₉ being Element of c₇ such that
E9: ( c₉ in c₈ & c₉ is_maximal_wrt c₈,the InternalRel of c₇ ) by E4, BAGORDER:7;
reconsider c₁₀ = c₉ as Element of c₂ by E9;
take c₁₀ ;
thus c₁₀ in c₂ by E9; :: according to WAYBEL_4:def 24
given c₁₁ being set such that E10: ( c₁₁ in c₂ & c₁₁ <> c₁₀ & [c₁₀,c₁₁] in c₁ ) ;
thus not verum by E9, E10, WAYBEL_4:def 24;

end;

definition

let c₁ be set ;
let c₂ be Relation;
func c₂ Maximal_in c₁ -> Subset of a₁ means :Def1: :: ARMSTRNG:def 1
for b₁ being set holds
( b₁ in a₃ iff b₁ is_maximal_wrt a₁,a₂ );
existence

proof

defpred S₁[ set ] means a₁ is_maximal_wrt c₁,c₂;
consider c₃ being set such that
E4: for b₁ being set holds
( b₁ in c₃ iff ( b₁ in c₁ & S₁[b₁] ) ) from XBOOLE_0:sch 1();
for b₁ being set holds
( b₁ in c₃ implies b₁ in c₁ ) by E4;
then reconsider c₄ = c₃ as Subset of c₁ by TARSKI:def 3;
take c₄ ;
let c₅ be set ;
thus ( c₅ in c₄ implies c₅ is_maximal_wrt c₁,c₂ ) by E4;
assume E5: c₅ is_maximal_wrt c₁,c₂ ;
then c₅ in c₁ by WAYBEL_4:def 24;
hence c₅ in c₄ by E4, E5;

end;

uniqueness

proof

defpred S₁[ set ] means a₁ is_maximal_wrt c₁,c₂;
thus for b₁, b₂ being Subset of c₁ holds
( ( for b₃ being set holds
( b₃ in b₁ iff S₁[b₃] ) ) & ( for b₃ being set holds
( b₃ in b₂ iff S₁[b₃] ) ) implies b₁ = b₂ ) from ARMSTRNG:sch 1();

end;

definition

let c₁ be non empty set ;
func /\-IRR c₁ -> Subset of a₁ means :Def3: :: ARMSTRNG:def 3
for b₁ being set holds
( b₁ in a₂ iff b₁ is_/\-irreducible_in a₁ );
existence

proof

set c₂ = { b₁ where B is Element of c₁ : b₁ is_/\-irreducible_in c₁ } ;
{ b₁ where B is Element of c₁ : b₁ is_/\-irreducible_in c₁ } c= c₁

proof

let c₃ be set ; :: according to TARSKI:def 3
assume c₃ in { b₁ where B is Element of c₁ : b₁ is_/\-irreducible_in c₁ } ;
then consider c₄ being Element of c₁ such that
E6: ( c₃ = c₄ & c₄ is_/\-irreducible_in c₁ ) ;
thus c₃ in c₁ by E6;

end;

then reconsider c₃ = { b₁ where B is Element of c₁ : b₁ is_/\-irreducible_in c₁ } as Subset of c₁ ;
take c₃ ;
let c₄ be set ;

hereby

assume c₄ in c₃ ;
then consider c₅ being Element of c₁ such that
E6: ( c₄ = c₅ & c₅ is_/\-irreducible_in c₁ ) ;
thus c₄ is_/\-irreducible_in c₁ by E6;

end;

assume E6: c₄ is_/\-irreducible_in c₁ ;
then c₄ in c₁ by Def2;
hence c₄ in c₃ by E6;

end;

uniqueness

proof

defpred S₁[ set ] means a₁ is_/\-irreducible_in c₁;
thus for b₁, b₂ being Subset of c₁ holds
( ( for b₃ being set holds
( b₃ in b₁ iff S₁[b₃] ) ) & ( for b₃ being set holds
( b₃ in b₂ iff S₁[b₃] ) ) implies b₁ = b₂ ) from ARMSTRNG:sch 1();

end;

scheme :: ARMSTRNG:sch 2
s2{ F₁() -> non empty finite set , P₁[ set ] } :

for b₁ being set holds
( b₁ in F₁() implies P₁[b₁] )

provided

E7: for b₁ being set holds
( b₁ is_/\-irreducible_in F₁() implies P₁[b₁] ) and E8: for b₁, b₂ being set holds
( b₁ in F₁() & b₂ in F₁() & P₁[b₁] & P₁[b₂] implies P₁[b₁ /\ b₂] )

proof

deffunc H₁( set ) -> set = { b₁ where B is Element of F₁() : a₁ c= b₁ } ;
given c₁ being set such that E9: c₁ in F₁() and
E10: not P₁[c₁] ;
defpred S₁[ Nat] means ex b₁ being Element of F₁() st
( Card H₁(b₁) = a₁ & not P₁[b₁] );
H₁(c₁) c= F₁()

proof

let c₂ be set ; :: according to TARSKI:def 3
assume c₂ in H₁(c₁) ;
then ex b₁ being Element of F₁() st
( c₂ = b₁ & c₁ c= b₁ ) ;
hence c₂ in F₁() ;

end;

then reconsider c₂ = H₁(c₁) as finite set by FINSET_1:13;
E11: ex b₁ being Nat st
S₁[b₁]

proof

take c₃ = card c₂;
reconsider c₄ = c₁ as Element of F₁() by E9;
take c₄ ;
thus Card H₁(c₄) = c₃ ;
thus not P₁[c₄] by E10;

end;

consider c₃ being Nat such that
E12: S₁[c₃] and
E13: for b₁ being Nat holds
( S₁[b₁] implies c₃ <= b₁ ) from NAT_1:sch 5(E11);
consider c₄ being Element of F₁() such that
E14: Card H₁(c₄) = c₃ and
E15: not P₁[c₄] by E12;

per cases ;

suppose c₄ is_/\-irreducible_in F₁() ;

hence not verum by E7, E15;

end;

suppose c₄ is_/\-reducible_in F₁() ;

then consider c₅, c₆ being set such that
E16: ( c₅ in F₁() & c₆ in F₁() ) and
E17: c₄ = c₅ /\ c₆ and
E18: ( c₄ <> c₅ & c₄ <> c₆ ) by Def2;
E19: ( c₄ c= c₅ & c₄ c= c₆ ) by E17, XBOOLE_1:17;
H₁(c₄) c= F₁()

proof

let c₇ be set ; :: according to TARSKI:def 3
assume c₇ in H₁(c₄) ;
then ex b₁ being Element of F₁() st
( c₇ = b₁ & c₄ c= b₁ ) ;
hence c₇ in F₁() ;

end;

then reconsider c₇ = H₁(c₄) as finite set by FINSET_1:13;
H₁(c₆) c= F₁()

proof

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in H₁(c₆) ;
then ex b₁ being Element of F₁() st
( c₈ = b₁ & c₆ c= b₁ ) ;
hence c₈ in F₁() ;

end;

then reconsider c₈ = H₁(c₆) as finite set by FINSET_1:13;
H₁(c₅) c= F₁()

proof

let c₉ be set ; :: according to TARSKI:def 3
assume c₉ in H₁(c₅) ;
then ex b₁ being Element of F₁() st
( c₉ = b₁ & c₅ c= b₁ ) ;
hence c₉ in F₁() ;

end;

then reconsider c₉ = H₁(c₅) as finite set by FINSET_1:13;
reconsider c₁₀ = c₆, c₁₁ = c₅ as Element of F₁() by E16;

E20: now

assume c₄ in c₉ ;
then ex b₁ being Element of F₁() st
( c₄ = b₁ & c₁₁ c= b₁ ) ;
hence not verum by E18, E19, XBOOLE_0:def 10;

end;

now

assume c₄ in c₈ ;
then ex b₁ being Element of F₁() st
( c₄ = b₁ & c₁₀ c= b₁ ) ;
hence not verum by E18, E19, XBOOLE_0:def 10;

end;

then E21: ( c₉ <> c₇ & c₈ <> c₇ ) by E20;
E22: c₉ c= c₇

proof

let c₁₂ be set ; :: according to TARSKI:def 3
assume c₁₂ in c₉ ;
then consider c₁₃ being Element of F₁() such that
E23: c₁₂ = c₁₃ and
E24: c₁₁ c= c₁₃ ;
c₄ c= c₁₃ by E19, E24, XBOOLE_1:1;
hence c₁₂ in c₇ by E23;

end;

c₈ c= c₇

proof

let c₁₂ be set ; :: according to TARSKI:def 3
assume c₁₂ in c₈ ;
then consider c₁₃ being Element of F₁() such that
E23: c₁₂ = c₁₃ and
E24: c₁₀ c= c₁₃ ;
c₄ c= c₁₃ by E19, E24, XBOOLE_1:1;
hence c₁₂ in c₇ by E23;

end;

then ( c₉ c< c₇ & c₈ c< c₇ ) by E21, E22, XBOOLE_0:def 8;
then ( card c₇ > card c₉ & card c₇ > card c₈ ) by TREES_1:24;
then ( P₁[c₁₁] & P₁[c₁₀] ) by E13, E14;
hence not verum by E8, E15, E17;

end;

proof

let c₁ be non empty finite set ;
let c₂ be Element of c₁;
defpred S₁[ set ] means ex b₁ being non empty Subset of c₁ st
( a₁ = meet b₁ & ( for b₂ being set holds
( b₂ in b₁ implies b₂ is_/\-irreducible_in c₁ ) ) );

E8: now

let c₃ be set ;
assume E9: c₃ is_/\-irreducible_in c₁ ;
thus S₁[c₃]

proof

c₃ in c₁ by E9, Def2;
then reconsider c₄ = {c₃} as non empty Subset of c₁ by ZFMISC_1:37;
take c₄ ;
thus c₃ = meet c₄ by SETFAM_1:11;
let c₅ be set ;
assume c₅ in c₄ ;
hence c₅ is_/\-irreducible_in c₁ by E9, TARSKI:def 1;

end;

E9: now

let c₃, c₄ be set ;
assume that
( c₃ in c₁ & c₄ in c₁ ) and
E10: S₁[c₃] and
E11: S₁[c₄] ;
consider c₅ being non empty Subset of c₁ such that
E12: c₃ = meet c₅ and
E13: for b₁ being set holds
( b₁ in c₅ implies b₁ is_/\-irreducible_in c₁ ) by E10;
consider c₆ being non empty Subset of c₁ such that
E14: c₄ = meet c₆ and
E15: for b₁ being set holds
( b₁ in c₆ implies b₁ is_/\-irreducible_in c₁ ) by E11;
reconsider c₇ = c₅ \/ c₆ as non empty Subset of c₁ ;

now

take c₈ = c₇;
thus c₃ /\ c₄ = meet c₈ by E12, E14, SETFAM_1:10;
let c₉ be set ;
assume E16: c₉ in c₈ ;

per cases by E16, XBOOLE_0:def 2;

suppose c₉ in c₅ ;

hence c₉ is_/\-irreducible_in c₁ by E13;

end;

suppose c₉ in c₆ ;

hence c₉ is_/\-irreducible_in c₁ by E15;

end;

hence S₁[c₃ /\ c₄] ;

end;

for b₁ being set holds
( b₁ in c₁ implies S₁[b₁] ) from ARMSTRNG:sch 2(E8, E9);
hence ex b₁ being non empty Subset of c₁ st
( c₂ = meet b₁ & ( for b₂ being set holds
( b₂ in b₁ implies b₂ is_/\-irreducible_in c₁ ) ) ) ;

end;

proof

let c₁ be set ;
let c₂ be non empty Subset-Family of c₁;
assume E10: c₂ is (B2) ;
let c₃ be Element of c₂;
assume that
E11: c₃ is_/\-irreducible_in c₂ and
E12: c₃ <> c₁ ;
let c₄ be finite Subset-Family of c₁;
assume that
E13: c₄ c= c₂ and
E14: c₃ = Intersect c₄ and
E15: not c₃ in c₄ ;
defpred S₁[ set ] means not ( ( for b₁, b₂ being Element of c₂ holds
not ( c₃ <> b₁ & c₃ <> b₂ & c₃ = b₁ /\ b₂ ) ) & ( for b₁ being Subset-Family of c₁ holds
( not a₁ = {} & not ( a₁ <> {} & a₁ = b₁ & Intersect b₁ <> c₃ & Intersect b₁ in c₂ ) ) ) );
E16: c₄ is finite ;
E17: S₁[ {} ] ;

E18: now

let c₅, c₆ be set ;
assume that
E19: c₅ in c₄ and
c₆ c= c₄ and
E20: S₁[c₆] ;

per cases by E20;

suppose ex b₁, b₂ being Element of c₂ st
( c₃ <> b₁ & c₃ <> b₂ & c₃ = b₁ /\ b₂ ) ;

hence S₁[c₆ \/ {c₅}] ;

end;

suppose not for b₁ being Subset-Family of c₁ holds
( not c₆ = {} & not ( c₆ = b₁ & Intersect b₁ <> c₃ & Intersect b₁ in c₂ ) ) ;

then consider c₇ being Subset-Family of c₁ such that
E21: ( c₆ = {} or ( c₆ <> {} & c₆ = c₇ & Intersect c₇ <> c₃ & Intersect c₇ in c₂ ) ) ;
thus S₁[c₆ \/ {c₅}]

proof

{c₅} c= bool c₁ by E19, ZFMISC_1:37;
then reconsider c₈ = {c₅} as Subset-Family of c₁ ;
E22: Intersect c₈ = meet c₈ by SETFAM_1:def 10;
then E23: Intersect c₈ = c₅ by SETFAM_1:11;

per cases by E21;

suppose c₆ = {} ;

hence S₁[c₆ \/ {c₅}] by E13, E15, E19, E23;

end;

suppose E24: ( c₆ <> {} & c₆ = c₇ & Intersect c₇ <> c₃ & Intersect c₇ in c₂ ) ;

then c₆ \/ c₈ c= bool c₁ by XBOOLE_1:8;
then reconsider c₉ = c₆ \/ c₈ as non empty Subset-Family of c₁ by XBOOLE_1:15;
E25: Intersect c₇ = meet c₇ by E24, SETFAM_1:def 10;
E26: Intersect c₉ = meet c₉ by SETFAM_1:def 10
.= (meet c₆) /\ (meet c₈) by E24, SETFAM_1:10 ;
thus S₁[c₆ \/ {c₅}]

proof

per cases ;

suppose E27: Intersect c₉ <> c₃ ;

Intersect c₉ in c₂ by E10, E13, E19, E22, E23, E24, E25, E26, FINSUB_1:def 2;
hence S₁[c₆ \/ {c₅}] by E27;

end;

suppose Intersect c₉ = c₃ ;

hence S₁[c₆ \/ {c₅}] by E13, E15, E19, E22, E23, E24, E25, E26;

end;

S₁[c₄] from FINSET_1:sch 2(E16, E17, E18);
then consider c₅ being Subset-Family of c₁ such that
E19: ( c₄ = {} or ( c₄ = c₅ & Intersect c₅ <> c₃ ) ) by E11, Def2;
thus not verum by E12, E14, E19, SETFAM_1:def 10;

end;

definition

let c₁ be Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func c₂ '&' c₃ -> Tuple of a₁,BOOLEAN means :Def5: :: ARMSTRNG:def 5
for b₁ being set holds
( b₁ in Seg a₁ implies a₄ . b₁ = (a₂ /. b₁) '&' (a₃ /. b₁) );
existence

proof

deffunc H₁( set ) -> Element of BOOLEAN = (c₂ /. a₁) '&' (c₃ /. a₁);
consider c₄ being FinSequence of BOOLEAN such that
E10: len c₄ = c₁ and
E11: for b₁ being Nat holds
( b₁ in Seg c₁ implies c₄ . b₁ = H₁(b₁) ) from FINSEQ_2:sch 1();
c₄ in BOOLEAN * by FINSEQ_1:def 11;
then c₄ in c₁ -tuples_on BOOLEAN by E10;
then reconsider c₅ = c₄ as Element of c₁ -tuples_on BOOLEAN ;
take c₅ ;
thus for b₁ being set holds
( b₁ in Seg c₁ implies c₅ . b₁ = (c₂ /. b₁) '&' (c₃ /. b₁) ) by E11;

end;

uniqueness

proof

let c₄, c₅ be Element of c₁ -tuples_on BOOLEAN ;
assume that
E10: for b₁ being set holds
( b₁ in Seg c₁ implies c₄ . b₁ = (c₂ /. b₁) '&' (c₃ /. b₁) ) and
E11: for b₁ being set holds
( b₁ in Seg c₁ implies c₅ . b₁ = (c₂ /. b₁) '&' (c₃ /. b₁) ) ;

now

E12: dom c₄ = Seg c₁ by Lemma1;
hence dom c₄ = dom c₅ by Lemma1;
let c₆ be set ;
assume E13: c₆ in dom c₄ ;
hence c₄ . c₆ = (c₂ /. c₆) '&' (c₃ /. c₆) by E10, E12
.= c₅ . c₆ by E11, E12, E13 ;

end;

hence c₄ = c₅ by FUNCT_1:9;

end;

commutativity ;

end;

proof

let c₁ be Nat;
let c₂ be Tuple of c₁,BOOLEAN ;
set c₃ = c₁ -BinarySequence 0;

now

let c₄ be set ;
E12: dom ((c₁ -BinarySequence 0) '&' c₂) = Seg c₁ by Lemma1;
hence dom ((c₁ -BinarySequence 0) '&' c₂) = dom (c₁ -BinarySequence 0) by Lemma1;
let c₅ be set ;
assume E13: c₅ in dom ((c₁ -BinarySequence 0) '&' c₂) ;
E14: dom (c₁ -BinarySequence 0) = Seg c₁ by Lemma1;
E15: c₁ -BinarySequence 0 = 0* c₁ by BINARI_3:26
.= c₁ |-> 0 by EUCLID:def 4 ;
then (c₁ -BinarySequence 0) . c₅ = 0 by E12, E13, FUNCOP_1:13;
then (c₁ -BinarySequence 0) /. c₅ = FALSE by E12, E13, E14, FINSEQ_4:def 4, MARGREL1:def 13;
hence ((c₁ -BinarySequence 0) '&' c₂) . c₅ = FALSE '&' (c₂ /. c₅) by E12, E13, Def5
.= FALSE by MARGREL1:49
.= (c₁ -BinarySequence 0) . c₅ by E12, E13, E15, FUNCOP_1:13, MARGREL1:def 13 ;

end;

hence (c₁ -BinarySequence 0) '&' c₂ = c₁ -BinarySequence 0 by FUNCT_1:9;

end;

proof

let c₁ be Nat;
let c₂ be Tuple of c₁,BOOLEAN ;
set c₃ = c₁ -BinarySequence 0;
set c₄ = 'not' (c₁ -BinarySequence 0);

now

let c₅ be set ;
E12: dom (('not' (c₁ -BinarySequence 0)) '&' c₂) = Seg c₁ by Lemma1;
hence E13: dom (('not' (c₁ -BinarySequence 0)) '&' c₂) = dom c₂ by Lemma1;
let c₆ be set ;
assume E14: c₆ in dom (('not' (c₁ -BinarySequence 0)) '&' c₂) ;
E15: c₁ -BinarySequence 0 = 0* c₁ by BINARI_3:26
.= c₁ |-> 0 by EUCLID:def 4 ;
E16: dom (c₁ -BinarySequence 0) = Seg c₁ by Lemma1;
(c₁ -BinarySequence 0) . c₆ = 0 by E12, E14, E15, FUNCOP_1:13;
then E17: (c₁ -BinarySequence 0) /. c₆ = FALSE by E12, E14, E16, FINSEQ_4:def 4, MARGREL1:def 13;
('not' (c₁ -BinarySequence 0)) /. c₆ = 'not' ((c₁ -BinarySequence 0) /. c₆) by E12, E14, BINARITH:def 4
.= TRUE by E17, MARGREL1:def 16 ;
hence (('not' (c₁ -BinarySequence 0)) '&' c₂) . c₆ = TRUE '&' (c₂ /. c₆) by E12, E14, Def5
.= c₂ /. c₆ by MARGREL1:50
.= c₂ . c₆ by E13, E14, FINSEQ_4:def 4 ;

end;

hence ('not' (c₁ -BinarySequence 0)) '&' c₂ = c₂ by FUNCT_1:9;

end;

proof

let c₁, c₂ be Nat;
assume E13: c₂ < c₁ ;
set c₃ = c₁ -BinarySequence (2 to_power c₂);
deffunc H₁( Nat) -> Element of a₁ -tuples_on BOOLEAN = a₁ -BinarySequence (2 to_power c₂);
defpred S₁[ Nat] means ( c₂ < a₁ implies H₁(a₁) . (c₂ + 1) = TRUE );
E14: S₁[0] ;

E15: now

let c₄ be Nat;
assume E16: S₁[c₄] ;

now

assume c₂ < c₄ + 1 ;
then E17: c₂ <= c₄ by NAT_1:38;

per cases by E17, REAL_1:def 5;

suppose E18: c₄ = 0 ;

then E19: c₂ = 0 by E17;
0* c₄ = c₄ |-> 0 by EUCLID:def 4;
then dom (0* c₄) = Seg c₄ by FUNCOP_1:19;
then E20: len (0* c₄) = c₄ by FINSEQ_1:def 3;
dom <*TRUE *> = Seg 1 by FINSEQ_1:55;
then E21: 1 in dom <*TRUE *> by FINSEQ_1:3;
thus H₁(c₄ + 1) . (c₂ + 1) = ((0* c₄) ^ <*TRUE