let X be set ; :: thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A ) )
assume that
A1: B is constant and
A2: the_value_of B = A ; :: thesis: for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
consider x being set such that
A3: x in dom B and
A4: A = B . x by A1, A2, FUNCT_1:def 18;
reconsider x = x as Element of NAT by A3;
dom B = NAT by FUNCT_2:def 1;
then for n being Element of NAT holds B . n = A by A1, A3, A4, FUNCT_1:def 16;
hence for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A ) by Th10, Th11; :: thesis: verum