:: FLANG_1 semantic presentation
begin
definition
let E be set ;
let a, b be Element of E ^omega ;
:: original: ^
redefine funca ^ b -> Element of E ^omega ;
coherence
a ^ b is Element of E ^omega by AFINSQ_1:def_7;
end;
definition
let E be set ;
:: original: <%>
redefine func <%> E -> Element of E ^omega ;
coherence
<%> E is Element of E ^omega by AFINSQ_1:def_7;
end;
definition
let E be non empty set ;
let e be Element of E;
:: original: <%
redefine func<%e%> -> Element of E ^omega ;
coherence
<%e%> is Element of E ^omega by AFINSQ_1:def_7;
end;
definition
let E be set ;
let a be Element of E ^omega ;
:: original: {
redefine func{a} -> Subset of (E ^omega);
coherence
{a} is Subset of (E ^omega) by SUBSET_1:33;
end;
definition
let E be set ;
let f be Function of NAT,(bool E);
let n be Nat;
:: original: .
redefine funcf . n -> Subset of E;
coherence
f . n is Subset of E
proof
n is Element of NAT by ORDINAL1:def_12;
then f . n in rng f by FUNCT_2:112;
hence f . n is Subset of E ; ::_thesis: verum
end;
end;
theorem Th1: :: FLANG_1:1
for n1, n, n2 being Nat st ( n1 > n or n2 > n ) holds
n1 + n2 > n
proof
let n1, n, n2 be Nat; ::_thesis: ( ( n1 > n or n2 > n ) implies n1 + n2 > n )
A1: ( n1 > n & n2 >= 0 implies n1 + n2 > n + 0 ) by XREAL_1:8;
A2: ( n1 >= 0 & n2 > n implies n1 + n2 > n + 0 ) by XREAL_1:8;
assume ( n1 > n or n2 > n ) ; ::_thesis: n1 + n2 > n
hence n1 + n2 > n by A1, A2; ::_thesis: verum
end;
theorem Th2: :: FLANG_1:2
for n1, n, n2 being Nat st n1 + n <= n2 + 1 & n > 0 holds
n1 <= n2
proof
let n1, n, n2 be Nat; ::_thesis: ( n1 + n <= n2 + 1 & n > 0 implies n1 <= n2 )
assume that
A1: n1 + n <= n2 + 1 and
A2: n > 0 ; ::_thesis: n1 <= n2
1 + 0 <= n by A2, NAT_1:13;
hence n1 <= n2 by A1, XREAL_1:8; ::_thesis: verum
end;
theorem Th3: :: FLANG_1:3
for n1, n2 being Nat holds
( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) )
proof
let n1, n2 be Nat; ::_thesis: ( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) )
thus ( not n1 + n2 = 1 or ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) ::_thesis: ( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 )
proof
assume A1: n1 + n2 = 1 ; ::_thesis: ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )
now__::_thesis:_(_n1_<=_1_&_n2_<=_1_&_not_(_n1_=_1_&_n2_=_0_)_implies_(_n1_=_0_&_n2_=_1_)_)
A2: ( n1 = 0 implies not n2 = 0 ) by A1;
assume A3: ( n1 <= 1 & n2 <= 1 ) ; ::_thesis: ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) )
( n1 = 1 implies not n2 = 1 ) by A1;
hence ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) by A3, A2, NAT_1:25; ::_thesis: verum
end;
hence ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) by A1, Th1; ::_thesis: verum
end;
thus ( ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) implies n1 + n2 = 1 ) ; ::_thesis: verum
end;
theorem Th4: :: FLANG_1:4
for x, E being set
for a, b being Element of E ^omega holds
( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )
proof
let x, E be set ; ::_thesis: for a, b being Element of E ^omega holds
( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )
let a, b be Element of E ^omega ; ::_thesis: ( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )
A1: ( {} ^ b = b & a ^ {} = a ) ;
thus ( not a ^ b = <%x%> or ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ::_thesis: ( ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) implies a ^ b = <%x%> )
proof
assume A2: a ^ b = <%x%> ; ::_thesis: ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) )
then len (a ^ b) = 1 by AFINSQ_1:34;
then (len a) + (len b) = 1 by AFINSQ_1:17;
then ( ( len a = 1 & b = <%> E ) or ( a = <%> E & len b = 1 ) ) by Th3;
hence ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) by A2, A1; ::_thesis: verum
end;
assume ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) ; ::_thesis: a ^ b = <%x%>
hence a ^ b = <%x%> by A1; ::_thesis: verum
end;
theorem Th5: :: FLANG_1:5
for E being set
for a being Element of E ^omega
for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )
proof
let E be set ; ::_thesis: for a being Element of E ^omega
for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )
let a be Element of E ^omega ; ::_thesis: for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )
let p, q be XFinSequence; ::_thesis: ( a = p ^ q implies ( p is Element of E ^omega & q is Element of E ^omega ) )
assume a = p ^ q ; ::_thesis: ( p is Element of E ^omega & q is Element of E ^omega )
then ( p is XFinSequence of & q is XFinSequence of ) by AFINSQ_1:31;
hence ( p is Element of E ^omega & q is Element of E ^omega ) by AFINSQ_1:def_7; ::_thesis: verum
end;
theorem Th6: :: FLANG_1:6
for x, E being set st <%x%> is Element of E ^omega holds
x in E
proof
let x, E be set ; ::_thesis: ( <%x%> is Element of E ^omega implies x in E )
assume <%x%> is Element of E ^omega ; ::_thesis: x in E
then rng <%x%> c= E by RELAT_1:def_19;
then {x} c= E by AFINSQ_1:33;
hence x in E by ZFMISC_1:31; ::_thesis: verum
end;
theorem Th7: :: FLANG_1:7
for E being set
for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )
proof
let E be set ; ::_thesis: for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )
let b be Element of E ^omega ; ::_thesis: for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )
let n be Nat; ::_thesis: ( len b = n + 1 implies ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> ) )
assume A1: len b = n + 1 ; ::_thesis: ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )
then b <> {} ;
then consider c9 being XFinSequence, x being set such that
A2: b = c9 ^ <%x%> by AFINSQ_1:40;
<%x%> is Element of E ^omega by A2, Th5;
then reconsider e = x as Element of E by Th6;
reconsider c = c9 as Element of E ^omega by A2, Th5;
take c ; ::_thesis: ex e being Element of E st
( len c = n & b = c ^ <%e%> )
take e ; ::_thesis: ( len c = n & b = c ^ <%e%> )
n + 1 = (len c) + (len <%x%>) by A1, A2, AFINSQ_1:17
.= (len c) + 1 by AFINSQ_1:33 ;
hence ( len c = n & b = c ^ <%e%> ) by A2; ::_thesis: verum
end;
theorem Th8: :: FLANG_1:8
for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being set st p = <%x%> ^ q
proof
let p be XFinSequence; ::_thesis: ( p <> {} implies ex q being XFinSequence ex x being set st p = <%x%> ^ q )
defpred S1[ Nat] means for p being XFinSequence st len p = $1 & p <> {} holds
ex q being XFinSequence ex x being set st p = <%x%> ^ q;
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let p be XFinSequence; ::_thesis: ( len p = n + 1 & p <> {} implies ex q being XFinSequence ex x being set st p = <%x%> ^ q )
assume that
A3: len p = n + 1 and
A4: p <> {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q
consider q being XFinSequence, x being set such that
A5: p = q ^ <%x%> by A4, AFINSQ_1:40;
A6: n + 1 = (len q) + (len <%x%>) by A3, A5, AFINSQ_1:17
.= (len q) + 1 by AFINSQ_1:33 ;
percases ( q = {} or q <> {} ) ;
suppose q = {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q
then p = {} ^ <%x%> by A5
.= <%x%> ^ {} ;
hence ex q being XFinSequence ex x being set st p = <%x%> ^ q ; ::_thesis: verum
end;
suppose q <> {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q
then consider r being XFinSequence, y being set such that
A7: q = <%y%> ^ r by A2, A6;
p = <%y%> ^ (r ^ <%x%>) by A5, A7, AFINSQ_1:27;
hence ex q being XFinSequence ex x being set st p = <%x%> ^ q ; ::_thesis: verum
end;
end;
end;
end;
A8: S1[ 0 ] ;
A9: for n being Nat holds S1[n] from NAT_1:sch_2(A8, A1);
A10: len p = len p ;
assume p <> {} ; ::_thesis: ex q being XFinSequence ex x being set st p = <%x%> ^ q
hence ex q being XFinSequence ex x being set st p = <%x%> ^ q by A9, A10; ::_thesis: verum
end;
theorem :: FLANG_1:9
for E being set
for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = <%e%> ^ c )
proof
let E be set ; ::_thesis: for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = <%e%> ^ c )
let b be Element of E ^omega ; ::_thesis: for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = <%e%> ^ c )
let n be Nat; ::_thesis: ( len b = n + 1 implies ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = <%e%> ^ c ) )
assume A1: len b = n + 1 ; ::_thesis: ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = <%e%> ^ c )
then b <> {} ;
then consider c9 being XFinSequence, x being set such that
A2: b = <%x%> ^ c9 by Th8;
<%x%> is Element of E ^omega by A2, Th5;
then reconsider e = x as Element of E by Th6;
reconsider c = c9 as Element of E ^omega by A2, Th5;
take c ; ::_thesis: ex e being Element of E st
( len c = n & b = <%e%> ^ c )
take e ; ::_thesis: ( len c = n & b = <%e%> ^ c )
n + 1 = (len c) + (len <%x%>) by A1, A2, AFINSQ_1:17
.= (len c) + 1 by AFINSQ_1:33 ;
hence ( len c = n & b = <%e%> ^ c ) by A2; ::_thesis: verum
end;
Lm1: for i, j being Nat
for p being XFinSequence st len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
by AFINSQ_1:61;
theorem :: FLANG_1:10
for E being set
for b being Element of E ^omega
for n, m being Nat st len b = n + m holds
ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
proof
let E be set ; ::_thesis: for b being Element of E ^omega
for n, m being Nat st len b = n + m holds
ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
let b be Element of E ^omega ; ::_thesis: for n, m being Nat st len b = n + m holds
ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
let n, m be Nat; ::_thesis: ( len b = n + m implies ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 ) )
assume len b = n + m ; ::_thesis: ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
then consider c19, c29 being XFinSequence such that
A1: ( len c19 = n & len c29 = m ) and
A2: b = c19 ^ c29 by Lm1;
reconsider c2 = c29 as Element of E ^omega by A2, Th5;
reconsider c1 = c19 as Element of E ^omega by A2, Th5;
take c1 ; ::_thesis: ex c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )
take c2 ; ::_thesis: ( len c1 = n & len c2 = m & b = c1 ^ c2 )
thus ( len c1 = n & len c2 = m & b = c1 ^ c2 ) by A1, A2; ::_thesis: verum
end;
theorem Th11: :: FLANG_1:11
for E being set
for a being Element of E ^omega st a ^ a = a holds
a = {}
proof
let E be set ; ::_thesis: for a being Element of E ^omega st a ^ a = a holds
a = {}
let a be Element of E ^omega ; ::_thesis: ( a ^ a = a implies a = {} )
assume a ^ a = a ; ::_thesis: a = {}
then (len a) + (len a) = len a by AFINSQ_1:17;
hence a = {} ; ::_thesis: verum
end;
begin
definition
let E be set ;
let A, B be Subset of (E ^omega);
funcA ^^ B -> Subset of (E ^omega) means :Def1: :: FLANG_1:def 1
for x being set holds
( x in it iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) );
existence
ex b1 being Subset of (E ^omega) st
for x being set holds
( x in b1 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) )
proof
defpred S1[ set ] means ex a, b being Element of E ^omega st
( a in A & b in B & $1 = a ^ b );
consider C being Subset of (E ^omega) such that
A1: for x being set holds
( x in C iff ( x in E ^omega & S1[x] ) ) from SUBSET_1:sch_1();
take C ; ::_thesis: for x being set holds
( x in C iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) )
thus for x being set holds
( x in C iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (E ^omega) st ( for x being set holds
( x in b1 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) holds
b1 = b2
proof
let C1, C2 be Subset of (E ^omega); ::_thesis: ( ( for x being set holds
( x in C1 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds
( x in C2 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) implies C1 = C2 )
assume that
A2: for x being set holds
( x in C1 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) and
A3: for x being set holds
( x in C2 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ; ::_thesis: C1 = C2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_C1_implies_x_in_C2_)_&_(_x_in_C2_implies_x_in_C1_)_)
let x be set ; ::_thesis: ( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) )
thus ( x in C1 implies x in C2 ) ::_thesis: ( x in C2 implies x in C1 )
proof
assume x in C1 ; ::_thesis: x in C2
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by A2;
hence x in C2 by A3; ::_thesis: verum
end;
assume x in C2 ; ::_thesis: x in C1
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by A3;
hence x in C1 by A2; ::_thesis: verum
end;
hence C1 = C2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines ^^ FLANG_1:def_1_:_
for E being set
for A, B, b4 being Subset of (E ^omega) holds
( b4 = A ^^ B iff for x being set holds
( x in b4 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) );
theorem Th12: :: FLANG_1:12
for E being set
for A, B being Subset of (E ^omega) holds
( A ^^ B = {} iff ( A = {} or B = {} ) )
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds
( A ^^ B = {} iff ( A = {} or B = {} ) )
let A, B be Subset of (E ^omega); ::_thesis: ( A ^^ B = {} iff ( A = {} or B = {} ) )
thus ( not A ^^ B = {} or A = {} or B = {} ) ::_thesis: ( ( A = {} or B = {} ) implies A ^^ B = {} )
proof
assume that
A1: A ^^ B = {} and
A2: A <> {} and
A3: B <> {} ; ::_thesis: contradiction
consider a being Element of E ^omega such that
A4: a in A by A2, SUBSET_1:4;
consider b being Element of E ^omega such that
A5: b in B by A3, SUBSET_1:4;
a ^ b in A ^^ B by A4, A5, Def1;
hence contradiction by A1; ::_thesis: verum
end;
assume A6: ( A = {} or B = {} ) ; ::_thesis: A ^^ B = {}
for x being set holds not x in A ^^ B
proof
given x being set such that A7: x in A ^^ B ; ::_thesis: contradiction
ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by A7, Def1;
hence contradiction by A6; ::_thesis: verum
end;
hence A ^^ B = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
theorem Th13: :: FLANG_1:13
for E being set
for A being Subset of (E ^omega) holds
( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A )
let A be Subset of (E ^omega); ::_thesis: ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A )
A1: for x being set st x in A ^^ {(<%> E)} holds
x in A
proof
let x be set ; ::_thesis: ( x in A ^^ {(<%> E)} implies x in A )
assume x in A ^^ {(<%> E)} ; ::_thesis: x in A
then consider a, d being Element of E ^omega such that
A2: a in A and
A3: ( d in {(<%> E)} & x = a ^ d ) by Def1;
x = a ^ {} by A3, TARSKI:def_1;
hence x in A by A2; ::_thesis: verum
end;
A4: for x being set st x in A holds
x in {(<%> E)} ^^ A
proof
let x be set ; ::_thesis: ( x in A implies x in {(<%> E)} ^^ A )
assume A5: x in A ; ::_thesis: x in {(<%> E)} ^^ A
ex d, a being Element of E ^omega st
( d in {(<%> E)} & a in A & x = d ^ a )
proof
reconsider a = x as Element of E ^omega by A5;
consider d being Element of E ^omega such that
A6: d = <%> E ;
take d ; ::_thesis: ex a being Element of E ^omega st
( d in {(<%> E)} & a in A & x = d ^ a )
take a ; ::_thesis: ( d in {(<%> E)} & a in A & x = d ^ a )
{} ^ a = a ;
hence ( d in {(<%> E)} & a in A & x = d ^ a ) by A5, A6, TARSKI:def_1; ::_thesis: verum
end;
hence x in {(<%> E)} ^^ A by Def1; ::_thesis: verum
end;
A7: for x being set st x in A holds
x in A ^^ {(<%> E)}
proof
let x be set ; ::_thesis: ( x in A implies x in A ^^ {(<%> E)} )
assume A8: x in A ; ::_thesis: x in A ^^ {(<%> E)}
ex a, d being Element of E ^omega st
( a in A & d in {(<%> E)} & x = a ^ d )
proof
reconsider a = x as Element of E ^omega by A8;
set d = <%> E;
take a ; ::_thesis: ex d being Element of E ^omega st
( a in A & d in {(<%> E)} & x = a ^ d )
take <%> E ; ::_thesis: ( a in A & <%> E in {(<%> E)} & x = a ^ (<%> E) )
a ^ {} = a ;
hence ( a in A & <%> E in {(<%> E)} & x = a ^ (<%> E) ) by A8, TARSKI:def_1; ::_thesis: verum
end;
hence x in A ^^ {(<%> E)} by Def1; ::_thesis: verum
end;
for x being set st x in {(<%> E)} ^^ A holds
x in A
proof
let x be set ; ::_thesis: ( x in {(<%> E)} ^^ A implies x in A )
assume x in {(<%> E)} ^^ A ; ::_thesis: x in A
then consider d, a being Element of E ^omega such that
A9: d in {(<%> E)} and
A10: a in A and
A11: x = d ^ a by Def1;
x = {} ^ a by A9, A11, TARSKI:def_1;
hence x in A by A10; ::_thesis: verum
end;
hence ( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A ) by A1, A4, A7, TARSKI:1; ::_thesis: verum
end;
theorem Th14: :: FLANG_1:14
for E being set
for A, B being Subset of (E ^omega) holds
( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds
( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )
let A, B be Subset of (E ^omega); ::_thesis: ( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )
thus ( A ^^ B = {(<%> E)} implies ( A = {(<%> E)} & B = {(<%> E)} ) ) ::_thesis: ( A = {(<%> E)} & B = {(<%> E)} implies A ^^ B = {(<%> E)} )
proof
assume that
A1: A ^^ B = {(<%> E)} and
A2: ( A <> {(<%> E)} or B <> {(<%> E)} ) ; ::_thesis: contradiction
<%> E in A ^^ B by A1, TARSKI:def_1;
then consider a, b being Element of E ^omega such that
A3: a in A and
A4: b in B and
<%> E = a ^ b by Def1;
A5: now__::_thesis:_for_x_being_set_st_(_x_in_A_or_x_in_B_)_holds_
not_x_<>_<%>_E
let x be set ; ::_thesis: ( ( x in A or x in B ) implies not x <> <%> E )
assume that
A6: ( x in A or x in B ) and
A7: x <> <%> E ; ::_thesis: contradiction
A8: now__::_thesis:_not_x_in_B
assume A9: x in B ; ::_thesis: contradiction
then reconsider xb = x as Element of E ^omega ;
A10: a ^ xb <> <%> E by A7, AFINSQ_1:30;
a ^ xb in A ^^ B by A3, A9, Def1;
hence contradiction by A1, A10, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_not_x_in_A
assume A11: x in A ; ::_thesis: contradiction
then reconsider xa = x as Element of E ^omega ;
A12: xa ^ b <> <%> E by A7, AFINSQ_1:30;
xa ^ b in A ^^ B by A4, A11, Def1;
hence contradiction by A1, A12, TARSKI:def_1; ::_thesis: verum
end;
hence contradiction by A6, A8; ::_thesis: verum
end;
then A13: for x being set holds
( x in B iff x = <%> E ) by A4;
for x being set holds
( x in A iff x = <%> E ) by A3, A5;
hence contradiction by A2, A13, TARSKI:def_1; ::_thesis: verum
end;
assume ( A = {(<%> E)} & B = {(<%> E)} ) ; ::_thesis: A ^^ B = {(<%> E)}
hence A ^^ B = {(<%> E)} by Th13; ::_thesis: verum
end;
theorem Th15: :: FLANG_1:15
for E being set
for A, B being Subset of (E ^omega) holds
( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds
( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )
let A, B be Subset of (E ^omega); ::_thesis: ( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )
thus ( <%> E in A ^^ B implies ( <%> E in A & <%> E in B ) ) ::_thesis: ( <%> E in A & <%> E in B implies <%> E in A ^^ B )
proof
assume <%> E in A ^^ B ; ::_thesis: ( <%> E in A & <%> E in B )
then ex a, b being Element of E ^omega st
( a in A & b in B & a ^ b = <%> E ) by Def1;
hence ( <%> E in A & <%> E in B ) by AFINSQ_1:30; ::_thesis: verum
end;
assume ( <%> E in A & <%> E in B ) ; ::_thesis: <%> E in A ^^ B
then {} ^ (<%> E) in A ^^ B by Def1;
hence <%> E in A ^^ B ; ::_thesis: verum
end;
theorem Th16: :: FLANG_1:16
for E being set
for B, A being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ B & A c= B ^^ A )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ B & A c= B ^^ A )
let B, A be Subset of (E ^omega); ::_thesis: ( <%> E in B implies ( A c= A ^^ B & A c= B ^^ A ) )
assume A1: <%> E in B ; ::_thesis: ( A c= A ^^ B & A c= B ^^ A )
thus A c= A ^^ B ::_thesis: A c= B ^^ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^^ B )
assume A2: x in A ; ::_thesis: x in A ^^ B
then reconsider xa = x as Element of E ^omega ;
xa ^ {} in A ^^ B by A1, A2, Def1;
hence x in A ^^ B ; ::_thesis: verum
end;
thus A c= B ^^ A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ^^ A )
assume A3: x in A ; ::_thesis: x in B ^^ A
then reconsider xa = x as Element of E ^omega ;
{} ^ xa in B ^^ A by A1, A3, Def1;
hence x in B ^^ A ; ::_thesis: verum
end;
end;
theorem Th17: :: FLANG_1:17
for E being set
for A, C, B, D being Subset of (E ^omega) st A c= C & B c= D holds
A ^^ B c= C ^^ D
proof
let E be set ; ::_thesis: for A, C, B, D being Subset of (E ^omega) st A c= C & B c= D holds
A ^^ B c= C ^^ D
let A, C, B, D be Subset of (E ^omega); ::_thesis: ( A c= C & B c= D implies A ^^ B c= C ^^ D )
assume A1: ( A c= C & B c= D ) ; ::_thesis: A ^^ B c= C ^^ D
thus A ^^ B c= C ^^ D ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ B or x in C ^^ D )
assume x in A ^^ B ; ::_thesis: x in C ^^ D
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by Def1;
hence x in C ^^ D by A1, Def1; ::_thesis: verum
end;
end;
theorem Th18: :: FLANG_1:18
for E being set
for A, B, C being Subset of (E ^omega) holds (A ^^ B) ^^ C = A ^^ (B ^^ C)
proof
let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds (A ^^ B) ^^ C = A ^^ (B ^^ C)
let A, B, C be Subset of (E ^omega); ::_thesis: (A ^^ B) ^^ C = A ^^ (B ^^ C)
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(A_^^_B)_^^_C_implies_x_in_A_^^_(B_^^_C)_)_&_(_x_in_A_^^_(B_^^_C)_implies_x_in_(A_^^_B)_^^_C_)_)
let x be set ; ::_thesis: ( ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) & ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C ) )
thus ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) ::_thesis: ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C )
proof
assume x in (A ^^ B) ^^ C ; ::_thesis: x in A ^^ (B ^^ C)
then consider ab, c being Element of E ^omega such that
A1: ab in A ^^ B and
A2: ( c in C & x = ab ^ c ) by Def1;
consider a, b being Element of E ^omega such that
A3: a in A and
A4: ( b in B & ab = a ^ b ) by A1, Def1;
( x = a ^ (b ^ c) & b ^ c in B ^^ C ) by A2, A4, Def1, AFINSQ_1:27;
hence x in A ^^ (B ^^ C) by A3, Def1; ::_thesis: verum
end;
assume x in A ^^ (B ^^ C) ; ::_thesis: x in (A ^^ B) ^^ C
then consider a, bc being Element of E ^omega such that
A5: a in A and
A6: bc in B ^^ C and
A7: x = a ^ bc by Def1;
consider b, c being Element of E ^omega such that
A8: b in B and
A9: c in C and
A10: bc = b ^ c by A6, Def1;
( x = (a ^ b) ^ c & a ^ b in A ^^ B ) by A5, A7, A8, A10, Def1, AFINSQ_1:27;
hence x in (A ^^ B) ^^ C by A9, Def1; ::_thesis: verum
end;
hence (A ^^ B) ^^ C = A ^^ (B ^^ C) by TARSKI:1; ::_thesis: verum
end;
theorem Th19: :: FLANG_1:19
for E being set
for A, B, C being Subset of (E ^omega) holds
( A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) )
proof
let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds
( A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) )
let A, B, C be Subset of (E ^omega); ::_thesis: ( A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) )
thus A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) ::_thesis: (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ (B /\ C) or x in (A ^^ B) /\ (A ^^ C) )
assume x in A ^^ (B /\ C) ; ::_thesis: x in (A ^^ B) /\ (A ^^ C)
then consider a, bc being Element of E ^omega such that
A1: a in A and
A2: bc in B /\ C and
A3: x = a ^ bc by Def1;
bc in C by A2, XBOOLE_0:def_4;
then A4: x in A ^^ C by A1, A3, Def1;
bc in B by A2, XBOOLE_0:def_4;
then x in A ^^ B by A1, A3, Def1;
hence x in (A ^^ B) /\ (A ^^ C) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B /\ C) ^^ A or x in (B ^^ A) /\ (C ^^ A) )
assume x in (B /\ C) ^^ A ; ::_thesis: x in (B ^^ A) /\ (C ^^ A)
then consider bc, a being Element of E ^omega such that
A5: bc in B /\ C and
A6: ( a in A & x = bc ^ a ) by Def1;
bc in C by A5, XBOOLE_0:def_4;
then A7: x in C ^^ A by A6, Def1;
bc in B by A5, XBOOLE_0:def_4;
then x in B ^^ A by A6, Def1;
hence x in (B ^^ A) /\ (C ^^ A) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
theorem Th20: :: FLANG_1:20
for E being set
for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )
proof
let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )
let A, B, C be Subset of (E ^omega); ::_thesis: ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )
A1: A ^^ (B \/ C) c= (A ^^ B) \/ (A ^^ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ (B \/ C) or x in (A ^^ B) \/ (A ^^ C) )
assume x in A ^^ (B \/ C) ; ::_thesis: x in (A ^^ B) \/ (A ^^ C)
then consider a, bc being Element of E ^omega such that
A2: a in A and
A3: bc in B \/ C and
A4: x = a ^ bc by Def1;
( bc in B or bc in C ) by A3, XBOOLE_0:def_3;
then ( x in A ^^ B or x in A ^^ C ) by A2, A4, Def1;
hence x in (A ^^ B) \/ (A ^^ C) by XBOOLE_0:def_3; ::_thesis: verum
end;
A5: (B \/ C) ^^ A c= (B ^^ A) \/ (C ^^ A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ C) ^^ A or x in (B ^^ A) \/ (C ^^ A) )
assume x in (B \/ C) ^^ A ; ::_thesis: x in (B ^^ A) \/ (C ^^ A)
then consider bc, a being Element of E ^omega such that
A6: bc in B \/ C and
A7: ( a in A & x = bc ^ a ) by Def1;
( bc in B or bc in C ) by A6, XBOOLE_0:def_3;
then ( x in B ^^ A or x in C ^^ A ) by A7, Def1;
hence x in (B ^^ A) \/ (C ^^ A) by XBOOLE_0:def_3; ::_thesis: verum
end;
C c= B \/ C by XBOOLE_1:7;
then A8: C ^^ A c= (B \/ C) ^^ A by Th17;
B c= B \/ C by XBOOLE_1:7;
then B ^^ A c= (B \/ C) ^^ A by Th17;
then A9: (B ^^ A) \/ (C ^^ A) c= (B \/ C) ^^ A by A8, XBOOLE_1:8;
C c= B \/ C by XBOOLE_1:7;
then A10: A ^^ C c= A ^^ (B \/ C) by Th17;
B c= B \/ C by XBOOLE_1:7;
then A ^^ B c= A ^^ (B \/ C) by Th17;
then (A ^^ B) \/ (A ^^ C) c= A ^^ (B \/ C) by A10, XBOOLE_1:8;
hence ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A ) by A1, A5, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th21: :: FLANG_1:21
for E being set
for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A )
proof
let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A )
let A, B, C be Subset of (E ^omega); ::_thesis: ( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A )
thus (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) ::_thesis: (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^^ B) \ (A ^^ C) or x in A ^^ (B \ C) )
assume A1: x in (A ^^ B) \ (A ^^ C) ; ::_thesis: x in A ^^ (B \ C)
then x in A ^^ B by XBOOLE_0:def_5;
then consider a, b being Element of E ^omega such that
A2: a in A and
A3: b in B and
A4: x = a ^ b by Def1;
A5: now__::_thesis:_(_not_b_in_C_implies_x_in_A_^^_(B_\_C)_)
assume not b in C ; ::_thesis: x in A ^^ (B \ C)
then b in B \ C by A3, XBOOLE_0:def_5;
hence x in A ^^ (B \ C) by A2, A4, Def1; ::_thesis: verum
end;
not x in A ^^ C by A1, XBOOLE_0:def_5;
hence x in A ^^ (B \ C) by A2, A4, A5, Def1; ::_thesis: verum
end;
thus (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B ^^ A) \ (C ^^ A) or x in (B \ C) ^^ A )
assume A6: x in (B ^^ A) \ (C ^^ A) ; ::_thesis: x in (B \ C) ^^ A
then x in B ^^ A by XBOOLE_0:def_5;
then consider b, a being Element of E ^omega such that
A7: b in B and
A8: ( a in A & x = b ^ a ) by Def1;
A9: now__::_thesis:_(_not_b_in_C_implies_x_in_(B_\_C)_^^_A_)
assume not b in C ; ::_thesis: x in (B \ C) ^^ A
then b in B \ C by A7, XBOOLE_0:def_5;
hence x in (B \ C) ^^ A by A8, Def1; ::_thesis: verum
end;
not x in C ^^ A by A6, XBOOLE_0:def_5;
hence x in (B \ C) ^^ A by A8, A9, Def1; ::_thesis: verum
end;
end;
theorem :: FLANG_1:22
for E being set
for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A )
proof
let E be set ; ::_thesis: for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A )
let A, B, C be Subset of (E ^omega); ::_thesis: ( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A )
(A ^^ B) \+\ (A ^^ C) = ((A ^^ B) \/ (A ^^ C)) \ ((A ^^ B) /\ (A ^^ C)) by XBOOLE_1:101
.= (A ^^ (B \/ C)) \ ((A ^^ B) /\ (A ^^ C)) by Th20 ;
then A1: (A ^^ B) \+\ (A ^^ C) c= (A ^^ (B \/ C)) \ (A ^^ (B /\ C)) by Th19, XBOOLE_1:34;
(B ^^ A) \+\ (C ^^ A) = ((B ^^ A) \/ (C ^^ A)) \ ((B ^^ A) /\ (C ^^ A)) by XBOOLE_1:101
.= ((B \/ C) ^^ A) \ ((B ^^ A) /\ (C ^^ A)) by Th20 ;
then A2: (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) ^^ A) \ ((B /\ C) ^^ A) by Th19, XBOOLE_1:34;
((B \/ C) ^^ A) \ ((B /\ C) ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by Th21;
then A3: (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by A2, XBOOLE_1:1;
(A ^^ (B \/ C)) \ (A ^^ (B /\ C)) c= A ^^ ((B \/ C) \ (B /\ C)) by Th21;
then (A ^^ B) \+\ (A ^^ C) c= A ^^ ((B \/ C) \ (B /\ C)) by A1, XBOOLE_1:1;
hence ( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A ) by A3, XBOOLE_1:101; ::_thesis: verum
end;
begin
definition
let E be set ;
let A be Subset of (E ^omega);
let n be Nat;
funcA |^ n -> Subset of (E ^omega) means :Def2: :: FLANG_1:def 2
ex concat being Function of NAT,(bool (E ^omega)) st
( it = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) );
existence
ex b1 being Subset of (E ^omega) ex concat being Function of NAT,(bool (E ^omega)) st
( b1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )
proof
defpred S1[ set , set , set ] means ex B, C being Subset of (E ^omega) st
( C = $3 & B = $2 & C = B ^^ A );
A1: for i being Element of NAT
for x being Element of bool (E ^omega) ex y being Element of bool (E ^omega) st S1[i,x,y]
proof
let i be Element of NAT ; ::_thesis: for x being Element of bool (E ^omega) ex y being Element of bool (E ^omega) st S1[i,x,y]
let x be Element of bool (E ^omega); ::_thesis: ex y being Element of bool (E ^omega) st S1[i,x,y]
take x ^^ A ; ::_thesis: S1[i,x,x ^^ A]
thus S1[i,x,x ^^ A] ; ::_thesis: verum
end;
consider f being Function of NAT,(bool (E ^omega)) such that
A2: ( f . 0 = {(<%> E)} & ( for i being Element of NAT holds S1[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch_2(A1);
consider C being Subset of (E ^omega) such that
A3: C = f . n ;
take C ; ::_thesis: ex concat being Function of NAT,(bool (E ^omega)) st
( C = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )
now__::_thesis:_for_i_being_Nat_holds_f_._(i_+_1)_=_(f_._i)_^^_A
let i be Nat; ::_thesis: f . (i + 1) = (f . i) ^^ A
reconsider j = i as Element of NAT by ORDINAL1:def_12;
ex B, C being Subset of (E ^omega) st
( C = f . (j + 1) & B = f . j & C = B ^^ A ) by A2;
hence f . (i + 1) = (f . i) ^^ A ; ::_thesis: verum
end;
hence ex concat being Function of NAT,(bool (E ^omega)) st
( C = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (E ^omega) st ex concat being Function of NAT,(bool (E ^omega)) st
( b1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being Function of NAT,(bool (E ^omega)) st
( b2 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) holds
b1 = b2
proof
let C1, C2 be Subset of (E ^omega); ::_thesis: ( ex concat being Function of NAT,(bool (E ^omega)) st
( C1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being Function of NAT,(bool (E ^omega)) st
( C2 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) implies C1 = C2 )
given f1 being Function of NAT,(bool (E ^omega)) such that A4: C1 = f1 . n and
A5: f1 . 0 = {(<%> E)} and
A6: for i being Nat holds f1 . (i + 1) = (f1 . i) ^^ A ; ::_thesis: ( for concat being Function of NAT,(bool (E ^omega)) holds
( not C2 = concat . n or not concat . 0 = {(<%> E)} or ex i being Nat st not concat . (i + 1) = (concat . i) ^^ A ) or C1 = C2 )
given f2 being Function of NAT,(bool (E ^omega)) such that A7: C2 = f2 . n and
A8: f2 . 0 = {(<%> E)} and
A9: for i being Nat holds f2 . (i + 1) = (f2 . i) ^^ A ; ::_thesis: C1 = C2
defpred S1[ Nat] means f1 . $1 = f2 . $1;
A10: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; ::_thesis: S1[k + 1]
f2 . (k + 1) = (f2 . k) ^^ A by A9;
hence S1[k + 1] by A6, A11; ::_thesis: verum
end;
A12: S1[ 0 ] by A5, A8;
for k being Nat holds S1[k] from NAT_1:sch_2(A12, A10);
hence C1 = C2 by A4, A7; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines |^ FLANG_1:def_2_:_
for E being set
for A being Subset of (E ^omega)
for n being Nat
for b4 being Subset of (E ^omega) holds
( b4 = A |^ n iff ex concat being Function of NAT,(bool (E ^omega)) st
( b4 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) );
theorem Th23: :: FLANG_1:23
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^ (n + 1) = (A |^ n) ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^ (n + 1) = (A |^ n) ^^ A
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A |^ (n + 1) = (A |^ n) ^^ A
let n be Nat; ::_thesis: A |^ (n + 1) = (A |^ n) ^^ A
consider concat being Function of NAT,(bool (E ^omega)) such that
A1: A |^ n = concat . n and
A2: concat . 0 = {(<%> E)} and
A3: for i being Nat holds concat . (i + 1) = (concat . i) ^^ A by Def2;
concat . (n + 1) = (A |^ n) ^^ A by A1, A3;
hence A |^ (n + 1) = (A |^ n) ^^ A by A2, A3, Def2; ::_thesis: verum
end;
theorem Th24: :: FLANG_1:24
for E being set
for A being Subset of (E ^omega) holds A |^ 0 = {(<%> E)}
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ 0 = {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: A |^ 0 = {(<%> E)}
ex concat being Function of NAT,(bool (E ^omega)) st
( A |^ 0 = concat . 0 & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by Def2;
hence A |^ 0 = {(<%> E)} ; ::_thesis: verum
end;
theorem Th25: :: FLANG_1:25
for E being set
for A being Subset of (E ^omega) holds A |^ 1 = A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ 1 = A
let A be Subset of (E ^omega); ::_thesis: A |^ 1 = A
consider concat being Function of NAT,(bool (E ^omega)) such that
A1: A |^ 1 = concat . 1 and
A2: ( concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by Def2;
thus A |^ 1 = concat . (0 + 1) by A1
.= {(<%> E)} ^^ A by A2
.= A by Th13 ; ::_thesis: verum
end;
theorem Th26: :: FLANG_1:26
for E being set
for A being Subset of (E ^omega) holds A |^ 2 = A ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A |^ 2 = A ^^ A
let A be Subset of (E ^omega); ::_thesis: A |^ 2 = A ^^ A
thus A |^ 2 = A |^ (1 + 1)
.= (A |^ 1) ^^ A by Th23
.= A ^^ A by Th25 ; ::_thesis: verum
end;
theorem Th27: :: FLANG_1:27
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {} iff ( n > 0 & A = {} ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {} iff ( n > 0 & A = {} ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( A |^ n = {} iff ( n > 0 & A = {} ) )
let n be Nat; ::_thesis: ( A |^ n = {} iff ( n > 0 & A = {} ) )
defpred S1[ Nat] means A |^ $1 = {} ;
thus ( A |^ n = {} implies ( n > 0 & A = {} ) ) ::_thesis: ( n > 0 & A = {} implies A |^ n = {} )
proof
assume that
A1: A |^ n = {} and
A2: ( n <= 0 or A <> {} ) ; ::_thesis: contradiction
A3: now__::_thesis:_not_A_<>_{}
defpred S2[ Nat] means A |^ $1 <> {} ;
assume A4: A <> {} ; ::_thesis: contradiction
A5: now__::_thesis:_for_n_being_Nat_st_S2[n]_holds_
S2[n_+_1]
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume S2[n] ; ::_thesis: S2[n + 1]
then consider a1 being Element of E ^omega such that
A6: a1 in A |^ n by SUBSET_1:4;
consider a2 being Element of E ^omega such that
A7: a2 in A by A4, SUBSET_1:4;
a1 ^ a2 in (A |^ n) ^^ A by A6, A7, Def1;
hence S2[n + 1] by Th23; ::_thesis: verum
end;
A |^ 0 = {(<%> E)} by Th24;
then A8: S2[ 0 ] ;
for n being Nat holds S2[n] from NAT_1:sch_2(A8, A5);
hence contradiction by A1; ::_thesis: verum
end;
now__::_thesis:_not_n_<=_0
assume n <= 0 ; ::_thesis: contradiction
then n = 0 ;
then A |^ n = {(<%> E)} by Th24;
hence contradiction by A1; ::_thesis: verum
end;
hence contradiction by A2, A3; ::_thesis: verum
end;
assume that
A9: n > 0 and
A10: A = {} ; ::_thesis: A |^ n = {}
A11: now__::_thesis:_for_m_being_Nat_st_1_<=_m_&_S1[m]_holds_
S1[m_+_1]
let m be Nat; ::_thesis: ( 1 <= m & S1[m] implies S1[m + 1] )
assume that
1 <= m and
S1[m] ; ::_thesis: S1[m + 1]
({} (E ^omega)) |^ (m + 1) = (({} (E ^omega)) |^ m) ^^ ({} (E ^omega)) by Th23
.= {} by Th12 ;
hence S1[m + 1] by A10; ::_thesis: verum
end;
A12: S1[1] by A10, Th25;
A13: for m being Nat st m >= 1 holds
S1[m] from NAT_1:sch_8(A12, A11);
n >= 0 + 1 by A9, NAT_1:13;
hence A |^ n = {} by A13; ::_thesis: verum
end;
theorem Th28: :: FLANG_1:28
for E being set
for n being Nat holds {(<%> E)} |^ n = {(<%> E)}
proof
let E be set ; ::_thesis: for n being Nat holds {(<%> E)} |^ n = {(<%> E)}
let n be Nat; ::_thesis: {(<%> E)} |^ n = {(<%> E)}
defpred S1[ Nat] means {(<%> E)} |^ $1 = {(<%> E)};
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
{(<%> E)} |^ (n + 1) = ({(<%> E)} |^ n) ^^ {(<%> E)} by Th23
.= {(<%> E)} by A2, Th13 ;
hence S1[n + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th24;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence {(<%> E)} |^ n = {(<%> E)} ; ::_thesis: verum
end;
theorem :: FLANG_1:29
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )
let n be Nat; ::_thesis: ( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )
thus ( not A |^ n = {(<%> E)} or n = 0 or A = {(<%> E)} ) ::_thesis: ( ( n = 0 or A = {(<%> E)} ) implies A |^ n = {(<%> E)} )
proof
assume A1: A |^ n = {(<%> E)} ; ::_thesis: ( n = 0 or A = {(<%> E)} )
now__::_thesis:_(_n_>_0_implies_A_=_{(<%>_E)}_)
assume n > 0 ; ::_thesis: A = {(<%> E)}
then consider m being Nat such that
A2: m + 1 = n by NAT_1:6;
A |^ n = (A |^ m) ^^ A by A2, Th23;
hence A = {(<%> E)} by A1, Th14; ::_thesis: verum
end;
hence ( n = 0 or A = {(<%> E)} ) ; ::_thesis: verum
end;
assume ( n = 0 or A = {(<%> E)} ) ; ::_thesis: A |^ n = {(<%> E)}
hence A |^ n = {(<%> E)} by Th24, Th28; ::_thesis: verum
end;
theorem Th30: :: FLANG_1:30
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
<%> E in A |^ n
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
<%> E in A |^ n
let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A holds
<%> E in A |^ n
let n be Nat; ::_thesis: ( <%> E in A implies <%> E in A |^ n )
defpred S1[ Nat] means <%> E in A |^ $1;
assume A1: <%> E in A ; ::_thesis: <%> E in A |^ n
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then <%> E in (A |^ n) ^^ A by A1, Th15;
hence S1[n + 1] by Th23; ::_thesis: verum
end;
A |^ 0 = {(<%> E)} by Th24;
then A3: S1[ 0 ] by TARSKI:def_1;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A2);
hence <%> E in A |^ n ; ::_thesis: verum
end;
theorem :: FLANG_1:31
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A |^ n & n > 0 holds
<%> E in A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A |^ n & n > 0 holds
<%> E in A
let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A |^ n & n > 0 holds
<%> E in A
let n be Nat; ::_thesis: ( <%> E in A |^ n & n > 0 implies <%> E in A )
assume that
A1: <%> E in A |^ n and
A2: n > 0 ; ::_thesis: <%> E in A
consider m being Nat such that
A3: m + 1 = n by A2, NAT_1:6;
A |^ n = (A |^ m) ^^ A by A3, Th23;
then ex a1, a2 being Element of E ^omega st
( a1 in A |^ m & a2 in A & a1 ^ a2 = <%> E ) by A1, Def1;
hence <%> E in A by AFINSQ_1:30; ::_thesis: verum
end;
theorem Th32: :: FLANG_1:32
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n)
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n)
let n be Nat; ::_thesis: (A |^ n) ^^ A = A ^^ (A |^ n)
defpred S1[ Nat] means (A |^ $1) ^^ A = A ^^ (A |^ $1);
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(A |^ (n + 1)) ^^ A = ((A |^ n) ^^ A) ^^ A by Th23
.= A ^^ ((A |^ n) ^^ A) by A2, Th18
.= A ^^ (A |^ (n + 1)) by Th23 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(A |^ 0) ^^ A = {(<%> E)} ^^ A by Th24
.= A by Th13
.= A ^^ {(<%> E)} by Th13
.= A ^^ (A |^ 0) by Th24 ;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence (A |^ n) ^^ A = A ^^ (A |^ n) ; ::_thesis: verum
end;
theorem Th33: :: FLANG_1:33
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n)
let m, n be Nat; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
defpred S1[ Nat] means for m, n being Nat st m + n <= $1 holds
A |^ (m + n) = (A |^ m) ^^ (A |^ n);
A1: now__::_thesis:_for_l_being_Nat_st_S1[l]_holds_
S1[l_+_1]
let l be Nat; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A2: S1[l] ; ::_thesis: S1[l + 1]
now__::_thesis:_for_m,_n_being_Nat_st_m_+_n_<=_l_+_1_holds_
A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)
let m, n be Nat; ::_thesis: ( m + n <= l + 1 implies A |^ (m + n) = (A |^ m) ^^ (A |^ n) )
A3: now__::_thesis:_(_m_+_n_<_l_+_1_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_)
assume m + n < l + 1 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
then m + n <= l by NAT_1:13;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A2; ::_thesis: verum
end;
A4: now__::_thesis:_(_m_+_n_=_l_+_1_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_)
assume A5: m + n = l + 1 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
A6: now__::_thesis:_(_n_=_0_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_)
assume A7: n = 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
thus A |^ (m + n) = (A |^ (l + 1)) ^^ {(<%> E)} by A5, Th13
.= (A |^ m) ^^ (A |^ n) by A5, A7, Th24 ; ::_thesis: verum
end;
A8: now__::_thesis:_(_m_>_0_&_n_>_0_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_)
assume that
A9: m > 0 and
A10: n > 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
consider k being Nat such that
A11: k + 1 = m by A9, NAT_1:6;
A |^ (m + n) = A |^ ((k + n) + 1) by A11
.= (A |^ (k + n)) ^^ A by Th23
.= A ^^ (A |^ (k + n)) by Th32
.= A ^^ ((A |^ k) ^^ (A |^ n)) by A2, A5, A11
.= (A ^^ (A |^ k)) ^^ (A |^ n) by Th18
.= ((A |^ k) ^^ A) ^^ (A |^ n) by Th32
.= ((A |^ k) ^^ (A |^ 1)) ^^ (A |^ n) by Th25
.= (A |^ m) ^^ (A |^ n) by A2, A5, A10, A11, Th2 ;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) ; ::_thesis: verum
end;
now__::_thesis:_(_m_=_0_implies_A_|^_(m_+_n)_=_(A_|^_m)_^^_(A_|^_n)_)
assume A12: m = 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
thus A |^ (m + n) = {(<%> E)} ^^ (A |^ (l + 1)) by A5, Th13
.= (A |^ m) ^^ (A |^ n) by A5, A12, Th24 ; ::_thesis: verum
end;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A6, A8; ::_thesis: verum
end;
assume m + n <= l + 1 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A4, A3, XXREAL_0:1; ::_thesis: verum
end;
hence S1[l + 1] ; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
let m, n be Nat; ::_thesis: ( m + n <= 0 implies A |^ (m + n) = (A |^ m) ^^ (A |^ n) )
assume A14: m + n <= 0 ; ::_thesis: A |^ (m + n) = (A |^ m) ^^ (A |^ n)
then A15: m = 0 ;
A16: m + n = 0 by A14;
hence A |^ (m + n) = (A |^ 0) ^^ {(<%> E)} by Th13
.= (A |^ m) ^^ (A |^ n) by A16, A15, Th24 ;
::_thesis: verum
end;
for l being Nat holds S1[l] from NAT_1:sch_2(A13, A1);
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) ; ::_thesis: verum
end;
theorem :: FLANG_1:34
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n)
let m, n be Nat; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
defpred S1[ Nat] means for m, n being Nat st m + n <= $1 holds
(A |^ m) |^ n = A |^ (m * n);
A1: now__::_thesis:_for_l_being_Nat_st_S1[l]_holds_
S1[l_+_1]
let l be Nat; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A2: S1[l] ; ::_thesis: S1[l + 1]
now__::_thesis:_for_m,_n_being_Nat_st_m_+_n_<=_l_+_1_holds_
(A_|^_m)_|^_n_=_A_|^_(m_*_n)
let m, n be Nat; ::_thesis: ( m + n <= l + 1 implies (A |^ m) |^ n = A |^ (m * n) )
A3: now__::_thesis:_(_m_+_n_<_l_+_1_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_)
assume m + n < l + 1 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
then m + n <= l by NAT_1:13;
hence (A |^ m) |^ n = A |^ (m * n) by A2; ::_thesis: verum
end;
A4: now__::_thesis:_(_m_+_n_=_l_+_1_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_)
assume A5: m + n = l + 1 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
A6: now__::_thesis:_(_m_>_0_&_n_>_0_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_)
assume that
m > 0 and
A7: n > 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
consider k being Nat such that
A8: k + 1 = n by A7, NAT_1:6;
A9: m + k <= l by A5, A8;
(A |^ m) |^ n = ((A |^ m) |^ k) ^^ (A |^ m) by A8, Th23
.= (A |^ (m * k)) ^^ (A |^ m) by A2, A9
.= A |^ ((m * k) + m) by Th33
.= A |^ (m * n) by A8 ;
hence (A |^ m) |^ n = A |^ (m * n) ; ::_thesis: verum
end;
A10: now__::_thesis:_(_n_=_0_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_)
assume A11: n = 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = {(<%> E)} by Th24
.= A |^ (m * n) by A11, Th24 ;
::_thesis: verum
end;
now__::_thesis:_(_m_=_0_implies_(A_|^_m)_|^_n_=_A_|^_(m_*_n)_)
assume A12: m = 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = {(<%> E)} |^ n by Th24
.= {(<%> E)} by Th28
.= A |^ (m * n) by A12, Th24 ;
::_thesis: verum
end;
hence (A |^ m) |^ n = A |^ (m * n) by A10, A6; ::_thesis: verum
end;
assume m + n <= l + 1 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = A |^ (m * n) by A4, A3, XXREAL_0:1; ::_thesis: verum
end;
hence S1[l + 1] ; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
let m, n be Nat; ::_thesis: ( m + n <= 0 implies (A |^ m) |^ n = A |^ (m * n) )
assume A14: m + n <= 0 ; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
then A15: m = 0 ;
n = 0 by A14;
hence (A |^ m) |^ n = {(<%> E)} by Th24
.= A |^ (m * n) by A15, Th24 ;
::_thesis: verum
end;
A16: for l being Nat holds S1[l] from NAT_1:sch_2(A13, A1);
now__::_thesis:_for_m,_n_being_Nat_holds_(A_|^_m)_|^_n_=_A_|^_(m_*_n)
let m, n be Nat; ::_thesis: (A |^ m) |^ n = A |^ (m * n)
reconsider l = m + n as Nat ;
m + n <= l ;
hence (A |^ m) |^ n = A |^ (m * n) by A16; ::_thesis: verum
end;
hence (A |^ m) |^ n = A |^ (m * n) ; ::_thesis: verum
end;
theorem Th35: :: FLANG_1:35
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A c= A |^ n
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A c= A |^ n
let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A & n > 0 holds
A c= A |^ n
let n be Nat; ::_thesis: ( <%> E in A & n > 0 implies A c= A |^ n )
assume that
A1: <%> E in A and
A2: n > 0 ; ::_thesis: A c= A |^ n
consider m being Nat such that
A3: m + 1 = n by A2, NAT_1:6;
<%> E in A |^ m by A1, Th30;
then A c= (A |^ m) ^^ A by Th16;
hence A c= A |^ n by A3, Th23; ::_thesis: verum
end;
theorem :: FLANG_1:36
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m > n holds
A |^ n c= A |^ m
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A & m > n holds
A |^ n c= A |^ m
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st <%> E in A & m > n holds
A |^ n c= A |^ m
let m, n be Nat; ::_thesis: ( <%> E in A & m > n implies A |^ n c= A |^ m )
assume that
A1: <%> E in A and
A2: m > n ; ::_thesis: A |^ n c= A |^ m
consider k being Nat such that
A3: n + k = m by A2, NAT_1:10;
<%> E in A |^ k by A1, Th30;
then A |^ n c= (A |^ k) ^^ (A |^ n) by Th16;
hence A |^ n c= A |^ m by A3, Th33; ::_thesis: verum
end;
theorem Th37: :: FLANG_1:37
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B holds
A |^ n c= B |^ n
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat st A c= B holds
A |^ n c= B |^ n
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B holds
A |^ n c= B |^ n
let n be Nat; ::_thesis: ( A c= B implies A |^ n c= B |^ n )
defpred S1[ Nat] means A |^ $1 c= B |^ $1;
assume A1: A c= B ; ::_thesis: A |^ n c= B |^ n
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
( (A |^ n) ^^ A = A |^ (n + 1) & (B |^ n) ^^ B = B |^ (n + 1) ) by Th23;
hence S1[n + 1] by A1, A3, Th17; ::_thesis: verum
end;
A |^ 0 = {(<%> E)} by Th24;
then A4: S1[ 0 ] by Th24;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A2);
hence A |^ n c= B |^ n ; ::_thesis: verum
end;
theorem :: FLANG_1:38
for E being set
for A, B being Subset of (E ^omega)
for n being Nat holds (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat holds (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n
let n be Nat; ::_thesis: (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n
( A |^ n c= (A \/ B) |^ n & B |^ n c= (A \/ B) |^ n ) by Th37, XBOOLE_1:7;
hence (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n by XBOOLE_1:8; ::_thesis: verum
end;
theorem :: FLANG_1:39
for E being set
for A, B being Subset of (E ^omega)
for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
let n be Nat; ::_thesis: (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
( (A /\ B) |^ n c= A |^ n & (A /\ B) |^ n c= B |^ n ) by Th37, XBOOLE_1:17;
hence (A /\ B) |^ n c= (A |^ n) /\ (B |^ n) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th40: :: FLANG_1:40
for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for m, n being Nat st a in C |^ m & b in C |^ n holds
a ^ b in C |^ (m + n)
proof
let E be set ; ::_thesis: for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for m, n being Nat st a in C |^ m & b in C |^ n holds
a ^ b in C |^ (m + n)
let C be Subset of (E ^omega); ::_thesis: for a, b being Element of E ^omega
for m, n being Nat st a in C |^ m & b in C |^ n holds
a ^ b in C |^ (m + n)
let a, b be Element of E ^omega ; ::_thesis: for m, n being Nat st a in C |^ m & b in C |^ n holds
a ^ b in C |^ (m + n)
let m, n be Nat; ::_thesis: ( a in C |^ m & b in C |^ n implies a ^ b in C |^ (m + n) )
assume ( a in C |^ m & b in C |^ n ) ; ::_thesis: a ^ b in C |^ (m + n)
then a ^ b in (C |^ m) ^^ (C |^ n) by Def1;
hence a ^ b in C |^ (m + n) by Th33; ::_thesis: verum
end;
begin
definition
let E be set ;
let A be Subset of (E ^omega);
funcA * -> Subset of (E ^omega) equals :: FLANG_1:def 3
union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } ;
coherence
union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } is Subset of (E ^omega)
proof
defpred S1[ set ] means ex n being Nat st $1 = A |^ n;
reconsider M = { B where B is Subset of (E ^omega) : S1[B] } as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
union M is Subset of (E ^omega) ;
hence union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } is Subset of (E ^omega) ; ::_thesis: verum
end;
end;
:: deftheorem defines * FLANG_1:def_3_:_
for E being set
for A being Subset of (E ^omega) holds A * = union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } ;
theorem Th41: :: FLANG_1:41
for E, x being set
for A being Subset of (E ^omega) holds
( x in A * iff ex n being Nat st x in A |^ n )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega) holds
( x in A * iff ex n being Nat st x in A |^ n )
let A be Subset of (E ^omega); ::_thesis: ( x in A * iff ex n being Nat st x in A |^ n )
thus ( x in A * implies ex n being Nat st x in A |^ n ) ::_thesis: ( ex n being Nat st x in A |^ n implies x in A * )
proof
defpred S1[ set ] means ex k being Nat st $1 = A |^ k;
assume x in A * ; ::_thesis: ex n being Nat st x in A |^ n
then consider X being set such that
A1: x in X and
A2: X in { B where B is Subset of (E ^omega) : ex k being Nat st B = A |^ k } by TARSKI:def_4;
A3: X in { B where B is Subset of (E ^omega) : S1[B] } by A2;
S1[X] from CARD_FIL:sch_1(A3);
hence ex n being Nat st x in A |^ n by A1; ::_thesis: verum
end;
given n being Nat such that A4: x in A |^ n ; ::_thesis: x in A *
defpred S1[ set ] means ex k being Nat st $1 = A |^ k;
consider B being Subset of (E ^omega) such that
A5: x in B and
A6: S1[B] by A4;
reconsider A = { C where C is Subset of (E ^omega) : S1[C] } as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
B in A by A6;
hence x in A * by A5, TARSKI:def_4; ::_thesis: verum
end;
theorem Th42: :: FLANG_1:42
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^ n c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^ n c= A *
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A |^ n c= A *
let n be Nat; ::_thesis: A |^ n c= A *
A |^ n in { B where B is Subset of (E ^omega) : ex k being Nat st B = A |^ k } ;
hence A |^ n c= A * by ZFMISC_1:74; ::_thesis: verum
end;
theorem Th43: :: FLANG_1:43
for E being set
for A being Subset of (E ^omega) holds A c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A c= A *
let A be Subset of (E ^omega); ::_thesis: A c= A *
A = A |^ 1 by Th25;
hence A c= A * by Th42; ::_thesis: verum
end;
theorem :: FLANG_1:44
for E being set
for A being Subset of (E ^omega) holds A ^^ A c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ^^ A c= A *
let A be Subset of (E ^omega); ::_thesis: A ^^ A c= A *
A ^^ A = A |^ 2 by Th26;
hence A ^^ A c= A * by Th42; ::_thesis: verum
end;
theorem Th45: :: FLANG_1:45
for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C * & b in C * holds
a ^ b in C *
proof
let E be set ; ::_thesis: for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C * & b in C * holds
a ^ b in C *
let C be Subset of (E ^omega); ::_thesis: for a, b being Element of E ^omega st a in C * & b in C * holds
a ^ b in C *
let a, b be Element of E ^omega ; ::_thesis: ( a in C * & b in C * implies a ^ b in C * )
assume that
A1: a in C * and
A2: b in C * ; ::_thesis: a ^ b in C *
consider k being Nat such that
A3: a in C |^ k by A1, Th41;
consider l being Nat such that
A4: b in C |^ l by A2, Th41;
a ^ b in C |^ (k + l) by A3, A4, Th40;
hence a ^ b in C * by Th41; ::_thesis: verum
end;
theorem Th46: :: FLANG_1:46
for E being set
for A, C, B being Subset of (E ^omega) st A c= C * & B c= C * holds
A ^^ B c= C *
proof
let E be set ; ::_thesis: for A, C, B being Subset of (E ^omega) st A c= C * & B c= C * holds
A ^^ B c= C *
let A, C, B be Subset of (E ^omega); ::_thesis: ( A c= C * & B c= C * implies A ^^ B c= C * )
assume A1: ( A c= C * & B c= C * ) ; ::_thesis: A ^^ B c= C *
thus A ^^ B c= C * ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ B or x in C * )
assume x in A ^^ B ; ::_thesis: x in C *
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by Def1;
hence x in C * by A1, Th45; ::_thesis: verum
end;
end;
theorem :: FLANG_1:47
for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
let A be Subset of (E ^omega); ::_thesis: ( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
thus ( not A * = {(<%> E)} or A = {} or A = {(<%> E)} ) ::_thesis: ( ( A = {} or A = {(<%> E)} ) implies A * = {(<%> E)} )
proof
A1: A c= A * by Th43;
assume that
A2: A * = {(<%> E)} and
A3: ( A <> {} & A <> {(<%> E)} ) ; ::_thesis: contradiction
ex x being set st
( x in A & x <> <%> E ) by A3, ZFMISC_1:35;
hence contradiction by A2, A1, TARSKI:def_1; ::_thesis: verum
end;
A4: now__::_thesis:_(_A_=_{}_implies_A_*_=_{(<%>_E)}_)
assume A5: A = {} ; ::_thesis: A * = {(<%> E)}
A6: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_
x_in_{(<%>_E)}
let x be set ; ::_thesis: ( x in A * implies x in {(<%> E)} )
assume x in A * ; ::_thesis: x in {(<%> E)}
then consider n being Nat such that
A7: x in A |^ n by Th41;
( n = 0 implies x in {(<%> E)} ) by A7, Th24;
hence x in {(<%> E)} by A5, A7, Th27; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in {(<%> E)} implies x in A * )
assume x in {(<%> E)} ; ::_thesis: x in A *
then x in A |^ 0 by Th24;
hence x in A * by Th41; ::_thesis: verum
end;
hence A * = {(<%> E)} by A6, TARSKI:1; ::_thesis: verum
end;
now__::_thesis:_(_A_=_{(<%>_E)}_implies_A_*_=_{(<%>_E)}_)
assume A8: A = {(<%> E)} ; ::_thesis: A * = {(<%> E)}
A9: A * c= {(<%> E)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * or x in {(<%> E)} )
assume x in A * ; ::_thesis: x in {(<%> E)}
then ex n being Nat st x in A |^ n by Th41;
hence x in {(<%> E)} by A8, Th28; ::_thesis: verum
end;
{(<%> E)} c= A *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(<%> E)} or x in A * )
assume x in {(<%> E)} ; ::_thesis: x in A *
then x in A |^ 0 by Th24;
hence x in A * by Th41; ::_thesis: verum
end;
hence A * = {(<%> E)} by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ( ( A = {} or A = {(<%> E)} ) implies A * = {(<%> E)} ) by A4; ::_thesis: verum
end;
theorem Th48: :: FLANG_1:48
for E being set
for A being Subset of (E ^omega) holds <%> E in A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds <%> E in A *
let A be Subset of (E ^omega); ::_thesis: <%> E in A *
{(<%> E)} = A |^ 0 by Th24;
then <%> E in A |^ 0 by TARSKI:def_1;
hence <%> E in A * by Th41; ::_thesis: verum
end;
theorem :: FLANG_1:49
for x, E being set
for A being Subset of (E ^omega) st A * = {x} holds
x = <%> E
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega) st A * = {x} holds
x = <%> E
let A be Subset of (E ^omega); ::_thesis: ( A * = {x} implies x = <%> E )
assume that
A1: A * = {x} and
A2: x <> <%> E ; ::_thesis: contradiction
reconsider a = x as Element of E ^omega by A1, ZFMISC_1:31;
x in A * by A1, ZFMISC_1:31;
then A3: a ^ a in A * by Th45;
a ^ a <> x by A2, Th11;
hence contradiction by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
theorem Th50: :: FLANG_1:50
for E, x being set
for A being Subset of (E ^omega)
for m being Nat st x in A |^ (m + 1) holds
( x in (A *) ^^ A & x in A ^^ (A *) )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega)
for m being Nat st x in A |^ (m + 1) holds
( x in (A *) ^^ A & x in A ^^ (A *) )
let A be Subset of (E ^omega); ::_thesis: for m being Nat st x in A |^ (m + 1) holds
( x in (A *) ^^ A & x in A ^^ (A *) )
let m be Nat; ::_thesis: ( x in A |^ (m + 1) implies ( x in (A *) ^^ A & x in A ^^ (A *) ) )
assume x in A |^ (m + 1) ; ::_thesis: ( x in (A *) ^^ A & x in A ^^ (A *) )
then A1: x in (A |^ m) ^^ A by Th23;
then consider a, b being Element of E ^omega such that
A2: a in A |^ m and
A3: ( b in A & x = a ^ b ) by Def1;
a in A * by A2, Th41;
hence x in (A *) ^^ A by A3, Def1; ::_thesis: x in A ^^ (A *)
x in A ^^ (A |^ m) by A1, Th32;
then consider a, b being Element of E ^omega such that
A4: a in A and
A5: b in A |^ m and
A6: x = a ^ b by Def1;
b in A * by A5, Th41;
hence x in A ^^ (A *) by A4, A6, Def1; ::_thesis: verum
end;
theorem :: FLANG_1:51
for E being set
for A being Subset of (E ^omega)
for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )
let A be Subset of (E ^omega); ::_thesis: for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )
let m be Nat; ::_thesis: ( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) )
thus A |^ (m + 1) c= (A *) ^^ A ::_thesis: A |^ (m + 1) c= A ^^ (A *)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m + 1) or x in (A *) ^^ A )
assume x in A |^ (m + 1) ; ::_thesis: x in (A *) ^^ A
hence x in (A *) ^^ A by Th50; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m + 1) or x in A ^^ (A *) )
assume x in A |^ (m + 1) ; ::_thesis: x in A ^^ (A *)
hence x in A ^^ (A *) by Th50; ::_thesis: verum
end;
theorem Th52: :: FLANG_1:52
for E, x being set
for A being Subset of (E ^omega) st ( x in (A *) ^^ A or x in A ^^ (A *) ) holds
x in A *
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega) st ( x in (A *) ^^ A or x in A ^^ (A *) ) holds
x in A *
let A be Subset of (E ^omega); ::_thesis: ( ( x in (A *) ^^ A or x in A ^^ (A *) ) implies x in A * )
A1: now__::_thesis:_for_x_being_set_st_x_in_A_^^_(A_*)_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in A ^^ (A *) implies x in A * )
assume x in A ^^ (A *) ; ::_thesis: x in A *
then consider a, b being Element of E ^omega such that
A2: a in A and
A3: b in A * and
A4: x = a ^ b by Def1;
consider n being Nat such that
A5: b in A |^ n by A3, Th41;
a in A |^ 1 by A2, Th25;
then a ^ b in A |^ (n + 1) by A5, Th40;
hence x in A * by A4, Th41; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_(A_*)_^^_A_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in (A *) ^^ A implies x in A * )
assume x in (A *) ^^ A ; ::_thesis: x in A *
then consider a, b being Element of E ^omega such that
A6: a in A * and
A7: b in A and
A8: x = a ^ b by Def1;
consider n being Nat such that
A9: a in A |^ n by A6, Th41;
b in A |^ 1 by A7, Th25;
then a ^ b in A |^ (n + 1) by A9, Th40;
hence x in A * by A8, Th41; ::_thesis: verum
end;
hence ( ( x in (A *) ^^ A or x in A ^^ (A *) ) implies x in A * ) by A1; ::_thesis: verum
end;
theorem :: FLANG_1:53
for E being set
for A being Subset of (E ^omega) holds
( (A *) ^^ A c= A * & A ^^ (A *) c= A * )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( (A *) ^^ A c= A * & A ^^ (A *) c= A * )
let A be Subset of (E ^omega); ::_thesis: ( (A *) ^^ A c= A * & A ^^ (A *) c= A * )
thus (A *) ^^ A c= A * ::_thesis: A ^^ (A *) c= A *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A *) ^^ A or x in A * )
assume x in (A *) ^^ A ; ::_thesis: x in A *
hence x in A * by Th52; ::_thesis: verum
end;
thus A ^^ (A *) c= A * ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^^ (A *) or x in A * )
assume x in A ^^ (A *) ; ::_thesis: x in A *
hence x in A * by Th52; ::_thesis: verum
end;
end;
theorem Th54: :: FLANG_1:54
for E being set
for A being Subset of (E ^omega) st <%> E in A holds
( A * = (A *) ^^ A & A * = A ^^ (A *) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) st <%> E in A holds
( A * = (A *) ^^ A & A * = A ^^ (A *) )
let A be Subset of (E ^omega); ::_thesis: ( <%> E in A implies ( A * = (A *) ^^ A & A * = A ^^ (A *) ) )
assume A1: <%> E in A ; ::_thesis: ( A * = (A *) ^^ A & A * = A ^^ (A *) )
A2: <%> E in A * by Th48;
A3: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_
(_x_in_(A_*)_^^_A_&_x_in_A_^^_(A_*)_)
let x be set ; ::_thesis: ( x in A * implies ( x in (A *) ^^ A & x in A ^^ (A *) ) )
assume x in A * ; ::_thesis: ( x in (A *) ^^ A & x in A ^^ (A *) )
then consider n being Nat such that
A4: x in A |^ n by Th41;
A5: now__::_thesis:_(_n_=_0_implies_(_x_in_(A_*)_^^_A_&_x_in_A_^^_(A_*)_)_)
assume n = 0 ; ::_thesis: ( x in (A *) ^^ A & x in A ^^ (A *) )
then x in {(<%> E)} by A4, Th24;
then x = <%> E by TARSKI:def_1;
hence ( x in (A *) ^^ A & x in A ^^ (A *) ) by A1, A2, Th15; ::_thesis: verum
end;
A6: now__::_thesis:_(_n_>_0_implies_x_in_A_^^_(A_*)_)
assume n > 0 ; ::_thesis: x in A ^^ (A *)
then ex m being Nat st m + 1 = n by NAT_1:6;
hence x in A ^^ (A *) by A4, Th50; ::_thesis: verum
end;
now__::_thesis:_(_n_>_0_implies_x_in_(A_*)_^^_A_)
assume n > 0 ; ::_thesis: x in (A *) ^^ A
then ex m being Nat st m + 1 = n by NAT_1:6;
hence x in (A *) ^^ A by A4, Th50; ::_thesis: verum
end;
hence ( x in (A *) ^^ A & x in A ^^ (A *) ) by A5, A6; ::_thesis: verum
end;
then A7: for x being set st x in A * holds
x in (A *) ^^ A ;
A8: for x being set st x in A * holds
x in A ^^ (A *) by A3;
for x being set holds
( ( x in (A *) ^^ A implies x in A * ) & ( x in A ^^ (A *) implies x in A * ) ) by Th52;
hence ( A * = (A *) ^^ A & A * = A ^^ (A *) ) by A7, A8, TARSKI:1; ::_thesis: verum
end;
theorem :: FLANG_1:55
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in A holds
( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )
let n be Nat; ::_thesis: ( <%> E in A implies ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) )
defpred S1[ Nat] means ( A * = (A *) ^^ (A |^ $1) & A * = (A |^ $1) ^^ (A *) );
A1: (A |^ 0) ^^ (A *) = {(<%> E)} ^^ (A *) by Th24
.= A * by Th13 ;
assume A2: <%> E in A ; ::_thesis: ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )
A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
A5: (A *) ^^ (A |^ (n + 1)) = (A *) ^^ ((A |^ n) ^^ A) by Th23
.= (A *) ^^ A by A4, Th18
.= A * by A2, Th54 ;
(A |^ (n + 1)) ^^ (A *) = ((A |^ n) ^^ A) ^^ (A *) by Th23
.= (A ^^ (A |^ n)) ^^ (A *) by Th32
.= A ^^ (A *) by A4, Th18
.= A * by A2, Th54 ;
hence S1[n + 1] by A5; ::_thesis: verum
end;
(A *) ^^ (A |^ 0) = (A *) ^^ {(<%> E)} by Th24
.= A * by Th13 ;
then A6: S1[ 0 ] by A1;
for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3);
hence ( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) ) ; ::_thesis: verum
end;
theorem Th56: :: FLANG_1:56
for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )
let A be Subset of (E ^omega); ::_thesis: ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )
A1: now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_\/_((A_*)_^^_A)_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in {(<%> E)} \/ ((A *) ^^ A) implies x in A * )
assume x in {(<%> E)} \/ ((A *) ^^ A) ; ::_thesis: x in A *
then ( x in {(<%> E)} or x in (A *) ^^ A ) by XBOOLE_0:def_3;
then ( x = <%> E or x in A * ) by Th52, TARSKI:def_1;
hence x in A * by Th48; ::_thesis: verum
end;
A2: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_
x_in_{(<%>_E)}_\/_((A_*)_^^_A)
let x be set ; ::_thesis: ( x in A * implies x in {(<%> E)} \/ ((A *) ^^ A) )
assume x in A * ; ::_thesis: x in {(<%> E)} \/ ((A *) ^^ A)
then consider n being Nat such that
A3: x in A |^ n by Th41;
A4: now__::_thesis:_(_n_>_0_implies_x_in_(A_*)_^^_A_)
assume n > 0 ; ::_thesis: x in (A *) ^^ A
then ex m being Nat st m + 1 = n by NAT_1:6;
hence x in (A *) ^^ A by A3, Th50; ::_thesis: verum
end;
( n = 0 implies x in {(<%> E)} ) by A3, Th24;
hence x in {(<%> E)} \/ ((A *) ^^ A) by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
A5: now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_
x_in_{(<%>_E)}_\/_(A_^^_(A_*))
let x be set ; ::_thesis: ( x in A * implies x in {(<%> E)} \/ (A ^^ (A *)) )
assume x in A * ; ::_thesis: x in {(<%> E)} \/ (A ^^ (A *))
then consider n being Nat such that
A6: x in A |^ n by Th41;
A7: now__::_thesis:_(_n_>_0_implies_x_in_A_^^_(A_*)_)
assume n > 0 ; ::_thesis: x in A ^^ (A *)
then ex m being Nat st m + 1 = n by NAT_1:6;
hence x in A ^^ (A *) by A6, Th50; ::_thesis: verum
end;
( n = 0 implies x in {(<%> E)} ) by A6, Th24;
hence x in {(<%> E)} \/ (A ^^ (A *)) by A7, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_\/_(A_^^_(A_*))_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in {(<%> E)} \/ (A ^^ (A *)) implies x in A * )
assume x in {(<%> E)} \/ (A ^^ (A *)) ; ::_thesis: x in A *
then ( x in {(<%> E)} or x in A ^^ (A *) ) by XBOOLE_0:def_3;
then ( x = <%> E or x in A * ) by Th52, TARSKI:def_1;
hence x in A * by Th48; ::_thesis: verum
end;
hence ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) by A2, A5, A1, TARSKI:1; ::_thesis: verum
end;
theorem Th57: :: FLANG_1:57
for E being set
for A being Subset of (E ^omega) holds A ^^ (A *) = (A *) ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ^^ (A *) = (A *) ^^ A
let A be Subset of (E ^omega); ::_thesis: A ^^ (A *) = (A *) ^^ A
A1: ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) by Th56;
now__::_thesis:_A_^^_(A_*)_=_(A_*)_^^_A
percases ( <%> E in A or not <%> E in A ) ;
supposeA2: <%> E in A ; ::_thesis: A ^^ (A *) = (A *) ^^ A
then A * = A ^^ (A *) by Th54;
hence A ^^ (A *) = (A *) ^^ A by A2, Th54; ::_thesis: verum
end;
supposeA3: not <%> E in A ; ::_thesis: A ^^ (A *) = (A *) ^^ A
then not <%> E in (A *) ^^ A by Th15;
then A4: {(<%> E)} misses (A *) ^^ A by ZFMISC_1:50;
not <%> E in A ^^ (A *) by A3, Th15;
then {(<%> E)} misses A ^^ (A *) by ZFMISC_1:50;
hence A ^^ (A *) = (A *) ^^ A by A1, A4, XBOOLE_1:71; ::_thesis: verum
end;
end;
end;
hence A ^^ (A *) = (A *) ^^ A ; ::_thesis: verum
end;
theorem :: FLANG_1:58
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n)
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n)
let n be Nat; ::_thesis: (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n)
defpred S1[ Nat] means (A |^ $1) ^^ (A *) = (A *) ^^ (A |^ $1);
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(A |^ (n + 1)) ^^ (A *) = ((A |^ n) ^^ A) ^^ (A *) by Th23
.= (A |^ n) ^^ (A ^^ (A *)) by Th18
.= (A |^ n) ^^ ((A *) ^^ A) by Th57
.= ((A *) ^^ (A |^ n)) ^^ A by A2, Th18
.= (A *) ^^ ((A |^ n) ^^ A) by Th18
.= (A *) ^^ (A |^ (n + 1)) by Th23 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(A |^ 0) ^^ (A *) = {(<%> E)} ^^ (A *) by Th24
.= A * by Th13
.= (A *) ^^ {(<%> E)} by Th13
.= (A *) ^^ (A |^ 0) by Th24 ;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n) ; ::_thesis: verum
end;
theorem Th59: :: FLANG_1:59
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B * holds
A |^ n c= B *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat st A c= B * holds
A |^ n c= B *
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B * holds
A |^ n c= B *
let n be Nat; ::_thesis: ( A c= B * implies A |^ n c= B * )
defpred S1[ Nat] means A |^ $1 c= B * ;
assume A1: A c= B * ; ::_thesis: A |^ n c= B *
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then (A |^ n) ^^ A c= B * by A1, Th46;
hence S1[n + 1] by Th23; ::_thesis: verum
end;
<%> E in B * by Th48;
then {(<%> E)} c= B * by ZFMISC_1:31;
then A3: S1[ 0 ] by Th24;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A2);
hence A |^ n c= B * ; ::_thesis: verum
end;
theorem Th60: :: FLANG_1:60
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
A * c= B *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B * holds
A * c= B *
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B * implies A * c= B * )
assume A1: A c= B * ; ::_thesis: A * c= B *
thus A * c= B * ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * or x in B * )
assume x in A * ; ::_thesis: x in B *
then consider n being Nat such that
A2: x in A |^ n by Th41;
A |^ n c= B * by A1, Th59;
hence x in B * by A2; ::_thesis: verum
end;
end;
theorem Th61: :: FLANG_1:61
for E being set
for A, B being Subset of (E ^omega) st A c= B holds
A * c= B *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B holds
A * c= B *
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B implies A * c= B * )
assume A1: A c= B ; ::_thesis: A * c= B *
B c= B * by Th43;
then A c= B * by A1, XBOOLE_1:1;
hence A * c= B * by Th60; ::_thesis: verum
end;
theorem Th62: :: FLANG_1:62
for E being set
for A being Subset of (E ^omega) holds (A *) * = A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A *) * = A *
let A be Subset of (E ^omega); ::_thesis: (A *) * = A *
( (A *) * c= A * & A * c= (A *) * ) by Th43, Th60;
hence (A *) * = A * by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FLANG_1:63
for E being set
for A being Subset of (E ^omega) holds (A *) ^^ (A *) = A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A *) ^^ (A *) = A *
let A be Subset of (E ^omega); ::_thesis: (A *) ^^ (A *) = A *
<%> E in A * by Th48;
then A1: A * c= (A *) ^^ (A *) by Th16;
(A *) ^^ (A *) c= A * by Th46;
hence (A *) ^^ (A *) = A * by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FLANG_1:64
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) * c= A * by Th42, Th60;
theorem Th65: :: FLANG_1:65
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A *) |^ n c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds (A *) |^ n c= A *
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A *) |^ n c= A *
let n be Nat; ::_thesis: (A *) |^ n c= A *
(A *) |^ n c= (A *) * by Th42;
hence (A *) |^ n c= A * by Th62; ::_thesis: verum
end;
theorem :: FLANG_1:66
for E being set
for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
(A *) |^ n = A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
(A *) |^ n = A *
let A be Subset of (E ^omega); ::_thesis: for n being Nat st n > 0 holds
(A *) |^ n = A *
let n be Nat; ::_thesis: ( n > 0 implies (A *) |^ n = A * )
<%> E in A * by Th48;
then A1: ( n > 0 implies A * c= (A *) |^ n ) by Th35;
(A *) |^ n c= A * by Th65;
hence ( n > 0 implies (A *) |^ n = A * ) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th67: :: FLANG_1:67
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
B * = (B \/ A) *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B * holds
B * = (B \/ A) *
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B * implies B * = (B \/ A) * )
defpred S1[ Nat] means (B \/ A) |^ $1 c= B * ;
assume A1: A c= B * ; ::_thesis: B * = (B \/ A) *
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
B c= B * by Th43;
then A4: B \/ A c= B * by A1, XBOOLE_1:8;
(B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by Th23;
hence S1[n + 1] by A3, A4, Th46; ::_thesis: verum
end;
( (B \/ A) |^ 0 = {(<%> E)} & <%> E in B * ) by Th24, Th48;
then A5: S1[ 0 ] by ZFMISC_1:31;
A6: for n being Nat holds S1[n] from NAT_1:sch_2(A5, A2);
A7: (B \/ A) * c= B *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ A) * or x in B * )
assume x in (B \/ A) * ; ::_thesis: x in B *
then consider n being Nat such that
A8: x in (B \/ A) |^ n by Th41;
(B \/ A) |^ n c= B * by A6;
hence x in B * by A8; ::_thesis: verum
end;
B * c= (B \/ A) * by Th61, XBOOLE_1:7;
hence B * = (B \/ A) * by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th68: :: FLANG_1:68
for E being set
for A being Subset of (E ^omega)
for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) *
let A be Subset of (E ^omega); ::_thesis: for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) *
let a be Element of E ^omega ; ::_thesis: ( a in A * implies A * = (A \/ {a}) * )
assume a in A * ; ::_thesis: A * = (A \/ {a}) *
then {a} c= A * by ZFMISC_1:31;
hence A * = (A \/ {a}) * by Th67; ::_thesis: verum
end;
theorem :: FLANG_1:69
for E being set
for A being Subset of (E ^omega) holds A * = (A \ {(<%> E)}) *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A * = (A \ {(<%> E)}) *
let A be Subset of (E ^omega); ::_thesis: A * = (A \ {(<%> E)}) *
thus (A \ {(<%> E)}) * = ((A \ {(<%> E)}) \/ {(<%> E)}) * by Th48, Th68
.= (A \/ {(<%> E)}) * by XBOOLE_1:39
.= A * by Th48, Th68 ; ::_thesis: verum
end;
theorem :: FLANG_1:70
for E being set
for A, B being Subset of (E ^omega) holds (A *) \/ (B *) c= (A \/ B) *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A *) \/ (B *) c= (A \/ B) *
let A, B be Subset of (E ^omega); ::_thesis: (A *) \/ (B *) c= (A \/ B) *
( A * c= (A \/ B) * & B * c= (A \/ B) * ) by Th61, XBOOLE_1:7;
hence (A *) \/ (B *) c= (A \/ B) * by XBOOLE_1:8; ::_thesis: verum
end;
theorem :: FLANG_1:71
for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) * c= (A *) /\ (B *)
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A /\ B) * c= (A *) /\ (B *)
let A, B be Subset of (E ^omega); ::_thesis: (A /\ B) * c= (A *) /\ (B *)
( (A /\ B) * c= A * & (A /\ B) * c= B * ) by Th61, XBOOLE_1:17;
hence (A /\ B) * c= (A *) /\ (B *) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th72: :: FLANG_1:72
for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A * iff <%x%> in A )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega) holds
( <%x%> in A * iff <%x%> in A )
let A be Subset of (E ^omega); ::_thesis: ( <%x%> in A * iff <%x%> in A )
thus ( <%x%> in A * implies <%x%> in A ) ::_thesis: ( <%x%> in A implies <%x%> in A * )
proof
defpred S1[ Nat] means <%x%> in A |^ $1;
assume that
A1: <%x%> in A * and
A2: not <%x%> in A ; ::_thesis: contradiction
A3: ex i being Nat st S1[i] by A1, Th41;
ex n1 being Nat st
( S1[n1] & ( for n2 being Nat st S1[n2] holds
n1 <= n2 ) ) from NAT_1:sch_5(A3);
then consider n1 being Nat such that
A4: S1[n1] and
A5: for n2 being Nat st S1[n2] holds
n1 <= n2 ;
A6: now__::_thesis:_not_n1_=_0
assume n1 = 0 ; ::_thesis: contradiction
then <%x%> in {(<%> E)} by A4, Th24;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
A7: now__::_thesis:_(_n1_>_1_implies_<%x%>_in_A_)
assume n1 > 1 ; ::_thesis: <%x%> in A
then consider n2 being Nat such that
A8: n2 + 1 = n1 by NAT_1:6;
<%x%> in (A |^ n2) ^^ A by A4, A8, Th23;
then consider a, b being Element of E ^omega such that
A9: a in A |^ n2 and
A10: ( b in A & <%x%> = a ^ b ) by Def1;
now__::_thesis:_(_a_=_<%x%>_implies_not_b_=_<%>_E_)
reconsider n2 = n2 as Element of NAT by ORDINAL1:def_12;
assume that
A11: a = <%x%> and
b = <%> E ; ::_thesis: contradiction
ex i being Element of NAT st
( S1[i] & n1 > i )
proof
take n2 ; ::_thesis: ( S1[n2] & n1 > n2 )
thus ( S1[n2] & n1 > n2 ) by A8, A9, A11, NAT_1:13; ::_thesis: verum
end;
hence contradiction by A5; ::_thesis: verum
end;
hence <%x%> in A by A10, Th4; ::_thesis: verum
end;
( n1 = 1 implies <%x%> in A ) by A4, Th25;
hence contradiction by A2, A7, A6, NAT_1:25; ::_thesis: verum
end;
assume <%x%> in A ; ::_thesis: <%x%> in A *
then <%x%> in A |^ 1 by Th25;
hence <%x%> in A * by Th41; ::_thesis: verum
end;
begin
definition
let E be set ;
func Lex E -> Subset of (E ^omega) means :Def4: :: FLANG_1:def 4
for x being set holds
( x in it iff ex e being Element of E st
( e in E & x = <%e%> ) );
existence
ex b1 being Subset of (E ^omega) st
for x being set holds
( x in b1 iff ex e being Element of E st
( e in E & x = <%e%> ) )
proof
defpred S1[ set ] means ex e being Element of E st
( e in E & $1 = <%e%> );
consider C being Subset of (E ^omega) such that
A1: for x being set holds
( x in C iff ( x in E ^omega & S1[x] ) ) from SUBSET_1:sch_1();
take C ; ::_thesis: for x being set holds
( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) )
for x being set holds
( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) )
proof
let x be set ; ::_thesis: ( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) )
thus ( x in C implies ex e being Element of E st
( e in E & x = <%e%> ) ) by A1; ::_thesis: ( ex e being Element of E st
( e in E & x = <%e%> ) implies x in C )
given e being Element of E such that A2: e in E and
A3: x = <%e%> ; ::_thesis: x in C
{e} c= E by A2, ZFMISC_1:31;
then rng <%e%> c= E by AFINSQ_1:33;
then <%e%> is XFinSequence of by RELAT_1:def_19;
then <%e%> is Element of E ^omega by AFINSQ_1:def_7;
hence x in C by A1, A2, A3; ::_thesis: verum
end;
hence for x being set holds
( x in C iff ex e being Element of E st
( e in E & x = <%e%> ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (E ^omega) st ( for x being set holds
( x in b1 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) & ( for x being set holds
( x in b2 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) holds
b1 = b2
proof
let C1, C2 be Subset of (E ^omega); ::_thesis: ( ( for x being set holds
( x in C1 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) & ( for x being set holds
( x in C2 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) implies C1 = C2 )
assume that
A4: for x being set holds
( x in C1 iff ex e being Element of E st
( e in E & x = <%e%> ) ) and
A5: for x being set holds
( x in C2 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ; ::_thesis: C1 = C2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_C1_implies_x_in_C2_)_&_(_x_in_C2_implies_x_in_C1_)_)
let x be set ; ::_thesis: ( ( x in C1 implies x in C2 ) & ( x in C2 implies x in C1 ) )
thus ( x in C1 implies x in C2 ) ::_thesis: ( x in C2 implies x in C1 )
proof
assume x in C1 ; ::_thesis: x in C2
then ex e being Element of E st
( e in E & x = <%e%> ) by A4;
hence x in C2 by A5; ::_thesis: verum
end;
assume x in C2 ; ::_thesis: x in C1
then ex e being Element of E st
( e in E & x = <%e%> ) by A5;
hence x in C1 by A4; ::_thesis: verum
end;
hence C1 = C2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Lex FLANG_1:def_4_:_
for E being set
for b2 being Subset of (E ^omega) holds
( b2 = Lex E iff for x being set holds
( x in b2 iff ex e being Element of E st
( e in E & x = <%e%> ) ) );
theorem Th73: :: FLANG_1:73
for E being set
for a being Element of E ^omega holds a in (Lex E) |^ (len a)
proof
let E be set ; ::_thesis: for a being Element of E ^omega holds a in (Lex E) |^ (len a)
let a be Element of E ^omega ; ::_thesis: a in (Lex E) |^ (len a)
defpred S1[ Nat] means for a being Element of E ^omega st len a = $1 holds
a in (Lex E) |^ $1;
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_b_being_Element_of_E_^omega_st_len_b_=_n_+_1_holds_
b_in_(Lex_E)_|^_(n_+_1)
let b be Element of E ^omega ; ::_thesis: ( len b = n + 1 implies b in (Lex E) |^ (n + 1) )
assume len b = n + 1 ; ::_thesis: b in (Lex E) |^ (n + 1)
then consider c being Element of E ^omega , e being Element of E such that
A3: len c = n and
A4: b = c ^ <%e%> by Th7;
<%e%> is Element of E ^omega by A4, Th5;
then e in E by Th6;
then <%e%> in Lex E by Def4;
then A5: <%e%> in (Lex E) |^ 1 by Th25;
c in (Lex E) |^ n by A2, A3;
hence b in (Lex E) |^ (n + 1) by A4, A5, Th40; ::_thesis: verum
end;
hence S1[n + 1] ; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
let a be Element of E ^omega ; ::_thesis: ( len a = 0 implies a in (Lex E) |^ 0 )
assume len a = 0 ; ::_thesis: a in (Lex E) |^ 0
then a = <%> E ;
then a in {(<%> E)} by TARSKI:def_1;
hence a in (Lex E) |^ 0 by Th24; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A6, A1);
hence a in (Lex E) |^ (len a) ; ::_thesis: verum
end;
theorem :: FLANG_1:74
for E being set holds (Lex E) * = E ^omega
proof
let E be set ; ::_thesis: (Lex E) * = E ^omega
A1: now__::_thesis:_for_x_being_set_st_x_in_E_^omega_holds_
x_in_(Lex_E)_*
let x be set ; ::_thesis: ( x in E ^omega implies x in (Lex E) * )
assume x in E ^omega ; ::_thesis: x in (Lex E) *
then reconsider a = x as Element of E ^omega ;
a in (Lex E) |^ (len a) by Th73;
hence x in (Lex E) * by Th41; ::_thesis: verum
end;
for x being set st x in (Lex E) * holds
x in E ^omega ;
hence (Lex E) * = E ^omega by A1, TARSKI:1; ::_thesis: verum
end;
theorem :: FLANG_1:75
for E being set
for A being Subset of (E ^omega) st A * = E ^omega holds
Lex E c= A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) st A * = E ^omega holds
Lex E c= A
let A be Subset of (E ^omega); ::_thesis: ( A * = E ^omega implies Lex E c= A )
assume A1: A * = E ^omega ; ::_thesis: Lex E c= A
thus Lex E c= A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lex E or x in A )
assume A2: x in Lex E ; ::_thesis: x in A
then ex e being Element of E st
( e in E & x = <%e%> ) by Def4;
hence x in A by A1, A2, Th72; ::_thesis: verum
end;
end;