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

( B . n = A & Union B = A & Intersection B = A ) by Th10, Th11; :: thesis: verum

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

hence
for n being Nat holds
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;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

( B . n = A & Union B = A & Intersection B = A ) by Th10, Th11; :: thesis: verum