:: FLANG_3 semantic presentation

begin

theorem :: FLANG_3:1
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let A be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let n be ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ;
func A |^.. n -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: FLANG_3:def 1
 union { B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where B is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ex m being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) <= m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Element of K6((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( ) set ) ;
end;

theorem :: FLANG_3:2
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ex m being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_3:3
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n, m being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:4
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) set ) iff ( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) set ) ) ) ;

theorem :: FLANG_3:5
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:6
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:7
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) holds
(A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:8
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:9
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:10
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) or <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_3:11
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff ( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) or n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: FLANG_3:12
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:13
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:14
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) <> <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) <> {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:15
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff ( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) or ( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) set ) ) ) ) ;

theorem :: FLANG_3:16
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:17
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:18
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:19
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n, m being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
(A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:20
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:21
for E being ( ( ) ( ) set )
for A, C, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:22
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:23
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:24
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:25
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, l, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:26
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:27
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:28
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:29
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:30
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:31
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:32
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:33
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, l, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
(A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:34
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
(A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:35
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:36
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:37
for E being ( ( ) ( ) set )
for C being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( V8() V33() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st a : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) in C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) in C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) ^ b : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( V8() V33() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:38
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) ;

theorem :: FLANG_3:39
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:40
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ( k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) or <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_3:41
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:42
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:43
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:44
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:45
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:46
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & ( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) or k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ) ) ;

theorem :: FLANG_3:47
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let A be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
func A + -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: FLANG_3:def 2
 union { B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where B is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ex n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Element of K6((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( ) set ) ;
end;

theorem :: FLANG_3:48
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ex n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_3:49
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:50
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:51
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) set ) iff A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) set ) ) ;

theorem :: FLANG_3:52
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:53
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:54
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:55
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:56
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:57
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:58
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:59
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:60
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:61
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:62
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:63
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) <> <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) <> {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:64
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:65
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:66
for E being ( ( ) ( ) set )
for C being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( V8() V33() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) st a : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) in C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) in C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) ^ b : ( ( ) ( V8() V33() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( V8() V33() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:67
for E being ( ( ) ( ) set )
for A, C, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:68
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:69
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) ;

theorem :: FLANG_3:70
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:71
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:72
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:73
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:74
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:75
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:76
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. 2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:77
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
(A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:78
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:79
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:80
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:81
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V32() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:82
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:83
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:84
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:85
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:86
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:87
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:88
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:89
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:90
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:91
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |^.. k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:92
for E being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:93
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_3:94
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:95
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ (B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) +) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_3:96
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) + : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;