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 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 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 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 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 12;
A5: dom B = NAT by FUNCT_2:def 1;
for n being Nat holds B . n = A
proof
let n be Nat; :: thesis: B . n = A
reconsider n = n as Element of NAT by ORDINAL1:def 12;
B . n = A by A1, A3, A4, FUNCT_1:def 10, A5;
hence B . n = A ; :: thesis: verum
end;
hence for n being Nat holds
( B . n = A & Union B = A & Intersection B = A ) by Th10, Th11; :: thesis: verum