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 ) )
consider F being Function of NAT,(bool X) such that
A1: ( rng F = {A,B,B} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = B ) ) by Th38;
take F ; :: thesis: ( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) )
{A,B,B} = {B,B,A} by ENUMSET1:100
.= {A,B} by ENUMSET1:70 ;
hence ( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) ) by A1, NAT_1:26; :: thesis: verum