let X be set ; :: thesis: for A, B being Subset of X ex F being Function of NAT,(bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) )
let A, B be Subset of X; :: thesis: ex F being Function of NAT,(bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being Element of 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 Element of 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 Element of NAT st 0 < n holds
(A followed_by B) . n = B ) ) by FUNCT_7:119, FUNCT_7:120, FUNCT_7:126; :: thesis: verum