let X be set ; :: thesis: for A, B being Subset of X ex F being sequence of (bool X) st

( rng F = {A,B} & F . 0 = A & ( for n being Nat st 0 < n holds

F . n = B ) )

let A, B be Subset of X; :: thesis: ex F being sequence of (bool X) st

( rng F = {A,B} & F . 0 = A & ( for n being Nat st 0 < n holds

F . n = B ) )

take A followed_by B ; :: thesis: ( rng (A followed_by B) = {A,B} & (A followed_by B) . 0 = A & ( for n being Nat st 0 < n holds

(A followed_by B) . n = B ) )

thus ( rng (A followed_by B) = {A,B} & (A followed_by B) . 0 = A & ( for n being Nat st 0 < n holds

(A followed_by B) . n = B ) ) by FUNCT_7:119, FUNCT_7:120, FUNCT_7:126; :: thesis: verum

( rng F = {A,B} & F . 0 = A & ( for n being Nat st 0 < n holds

F . n = B ) )

let A, B be Subset of X; :: thesis: ex F being sequence of (bool X) st

( rng F = {A,B} & F . 0 = A & ( for n being Nat st 0 < n holds

F . n = B ) )

take A followed_by B ; :: thesis: ( rng (A followed_by B) = {A,B} & (A followed_by B) . 0 = A & ( for n being Nat st 0 < n holds

(A followed_by B) . n = B ) )

thus ( rng (A followed_by B) = {A,B} & (A followed_by B) . 0 = A & ( for n being Nat st 0 < n holds

(A followed_by B) . n = B ) ) by FUNCT_7:119, FUNCT_7:120, FUNCT_7:126; :: thesis: verum