let n be Nat; :: thesis: for AA being Subset-Family of (COMPLEX n) st ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) holds
for A being Subset of (COMPLEX n) st A = union AA holds
A is open
let AA be Subset-Family of (COMPLEX n); :: thesis: ( ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) implies for A being Subset of (COMPLEX n) st A = union AA holds
A is open )
assume A1: for A being Subset of (COMPLEX n) st A in AA holds
A is open ; :: thesis: for A being Subset of (COMPLEX n) st A = union AA holds
A is open
let A be Subset of (COMPLEX n); :: thesis: ( A = union AA implies A is open )
assume A2: A = union AA ; :: thesis: A is open
let x be Element of COMPLEX n; :: according to SEQ_4:def 14 :: thesis: ( x in A implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) )
assume x in A ; :: thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) )
then consider B being set such that
A3: x in B and
A4: B in AA by A2, TARSKI:def 4;
reconsider B = B as Subset of (COMPLEX n) by A4;
B is open by A1, A4;
then consider r being Real such that
A5: 0 < r and
A6: for z being Element of COMPLEX n st |.z.| < r holds
x + z in B by A3;
take r ; :: thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) )
thus 0 < r by A5; :: thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in A
let z be Element of COMPLEX n; :: thesis: ( |.z.| < r implies x + z in A )
assume |.z.| < r ; :: thesis: x + z in A
then x + z in B by A6;
hence x + z in A by A2, A4, TARSKI:def 4; :: thesis: verum