:: FLANG_1 semantic presentation

begin

definition
let E be ( ( ) ( ) set ) ;
let a, b be ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) ;
:: original: ^
redefine func a ^ b -> ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
:: original: <%>
redefine func <%> E -> ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) ;
end;

definition
let E be ( ( non empty ) ( non empty ) set ) ;
let e be ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) ;
:: original: <%
redefine func <%e%> -> ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
let a be ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) ;
:: original: {
redefine func {a} -> ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

definition
let E be ( ( ) ( ) set ) ;
let f be ( ( Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool E : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K7(K7(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( bool E : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K7(K7(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool E : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K7(K7(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool E : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K7(K7(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;
let n be ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ;
:: original: .
redefine func f . n -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: FLANG_1:1
for n1, n, n2 being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st ( n1 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) or n2 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) holds
n1 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + n2 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) set ) > n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ;

theorem :: FLANG_1:2
for n1, n, n2 being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st n1 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) set ) <= n2 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) & n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
n1 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) <= n2 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ;

theorem :: FLANG_1:3
for n1, n2 being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds
( n1 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + n2 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) set ) = 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) iff ( ( n1 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) = 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & n2 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) = 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) or ( n1 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) = 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & n2 : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) = 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ) ) ;

theorem :: FLANG_1:4
for x, E being ( ( ) ( ) set )
for a, b being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) holds
( a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) ^ b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) = <%x : ( ( ) ( ) set ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) iff ( ( a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) & b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) = <%x : ( ( ) ( ) set ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) ) or ( b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) & a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) = <%x : ( ( ) ( ) set ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) ) ) ) ;

theorem :: FLANG_1:5
for E being ( ( ) ( ) set )
for a being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) )
for p, q being ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) st a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) = p : ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) ^ q : ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) : ( ( V9() V16() Function-like ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) holds
( p : ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) is ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) & q : ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) is ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ) ;

theorem :: FLANG_1:6
for x, E being ( ( ) ( ) set ) st <%x : ( ( ) ( ) set ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) is ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) holds
x : ( ( ) ( ) set ) in E : ( ( ) ( ) set ) ;

theorem :: FLANG_1:7
for E being ( ( ) ( ) set )
for b being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st len b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) = n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) holds
ex c being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ex e being ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) st
( len c : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) = n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) & b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) = c : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ^ <%e : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) : ( ( V9() V16() Function-like ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) ) ;

theorem :: FLANG_1:8
for p being ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) st p : ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) <> {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) holds
ex q being ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) ex x being ( ( ) ( ) set ) st p : ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) = <%x : ( ( ) ( ) set ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) ^ q : ( ( V9() V16() Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) XFinSequence) : ( ( V9() V16() Function-like ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) ;

theorem :: FLANG_1:9
for E being ( ( ) ( ) set )
for b being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st len b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) = n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) holds
ex c being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ex e being ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) st
( len c : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) = n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) & b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) = <%e : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) ^ c : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( V9() V16() Function-like ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) ) ;

theorem :: FLANG_1:10
for E being ( ( ) ( ) set )
for b being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) )
for n, m being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st len b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) = n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) set ) holds
ex c1, c2 being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) st
( len c1 : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) = n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) & len c2 : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) = m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) & b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) = c1 : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ^ c2 : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ) ;

theorem :: FLANG_1:11
for E being ( ( ) ( ) set )
for a being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) st a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ^ a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) = a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) holds
a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) = {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let A, B be ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;
func A ^^ B -> ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) means :: FLANG_1:def 1
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff ex a, b being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) st
( a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) in A : ( ( V9() V16() V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) & b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) in B : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) = a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) ^ b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) V20(E : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) ) );
end;

theorem :: FLANG_1:12
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) iff ( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) or B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) ) ) ;

theorem :: FLANG_1:13
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:14
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) iff ( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_1:15
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) iff ( <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_1:16
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:17
for E being ( ( ) ( ) set )
for A, C, B, D being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= D : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ D : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:18
for E being ( ( ) ( ) set )
for A, B, C being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:19
for E being ( ( ) ( ) set )
for A, B, C being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ (C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:20
for E being ( ( ) ( ) set )
for A, B, C being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ (C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:21
for E being ( ( ) ( ) set )
for A, B, C being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \ (C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:22
for E being ( ( ) ( ) set )
for A, B, C being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \+\ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \+\ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \+\ (C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \+\ C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let A be ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;
let n be ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ;
func A |^ n -> ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) means :: FLANG_1:def 2
 ex concat being ( ( Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) st
( it : ( ( ) ( ) set ) = concat : ( ( Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & concat : ( ( Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(E : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) & ( for i being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds concat : ( ( Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . (i : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (concat : ( ( Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) , bool (E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) : ( ( ) ( non empty ) Element of K7(K7((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . i : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( V9() V16() V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: FLANG_1:23
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:24
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:25
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:26
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ 2 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:27
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) iff ( n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) ) ) ;

theorem :: FLANG_1:28
for E being ( ( ) ( ) set )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:29
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) iff ( n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) = 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) or A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_1:30
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
<%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:31
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
<%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:32
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:33
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:34
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) * n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:35
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:36
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:37
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:38
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:39
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:40
for E being ( ( ) ( ) set )
for C being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) )
for m, n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ^ b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let A be ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;
func A * -> ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) equals :: FLANG_1:def 3
 union { B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) where B is ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ex n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( V9() V16() V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) set ) ;
end;

theorem :: FLANG_1:41
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) iff ex n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st x : ( ( ) ( ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:42
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:43
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:44
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:45
for E being ( ( ) ( ) set )
for C being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) st a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ^ b : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:46
for E being ( ( ) ( ) set )
for A, C, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:47
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) iff ( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) set ) or A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_1:48
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:49
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty V33() ) set ) holds
x : ( ( ) ( ) set ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b2 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b2 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b2 : ( ( ) ( ) set ) )) ) ;

theorem :: FLANG_1:50
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for m being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st x : ( ( ) ( ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:51
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for m being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) + 1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:52
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st ( x : ( ( ) ( ) set ) in (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) or x : ( ( ) ( ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) holds
x : ( ( ) ( ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:53
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:54
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:55
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:56
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) \/ ((A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_1:57
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:58
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:59
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:60
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:61
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:62
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:63
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:64
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:65
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:66
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) st n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) > 0 : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
(A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V11() ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Nat) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:67
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:68
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) st a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ {a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:69
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \ {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like one-to-one constant functional V33() V34() V37() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty functional V33() V37() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:70
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:71
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) /\ (B : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( functional ) Element of K7((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:72
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) holds
( <%x : ( ( ) ( ) set ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) iff <%x : ( ( ) ( ) set ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
func Lex E -> ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) means :: FLANG_1:def 4
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( V9() V16() V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V51() ) set ) iff ex e being ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) st
( e : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) in E : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) = <%e : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) %> : ( ( V16() Function-like ) ( non empty V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) Function-like V33() V40(1 : ( ( ) ( V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) ) );
end;

theorem :: FLANG_1:73
for E being ( ( ) ( ) set )
for a being ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) holds a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) in (Lex E : ( ( ) ( ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) |^ (len a : ( ( ) ( V9() V16() V19( NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20(b1 : ( ( ) ( ) set ) ) Function-like V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ) ) : ( ( ) ( V1() V5() V6() V7() V11() V12() ext-real non negative ) Element of NAT : ( ( ) ( non empty V5() V6() V7() ) Element of K7(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_1:74
for E being ( ( ) ( ) set ) holds (Lex E : ( ( ) ( ) set ) ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) ;

theorem :: FLANG_1:75
for E being ( ( ) ( ) set )
for A being ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) = E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty functional ) M9(b1 : ( ( ) ( ) set ) )) holds
Lex E : ( ( ) ( ) set ) : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;