let X be set ; :: thesis: for A, B, C being Subset of X ex F being sequence of (bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
let A, B, C be Subset of X; :: thesis: ex F being sequence of (bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
take (A,B) followed_by C ; :: thesis: ( rng ((A,B) followed_by C) = {A,B,C} & ((A,B) followed_by C) . 0 = A & ((A,B) followed_by C) . 1 = B & ( for n being Element of NAT st 1 < n holds
((A,B) followed_by C) . n = C ) )
thus ( rng ((A,B) followed_by C) = {A,B,C} & ((A,B) followed_by C) . 0 = A & ((A,B) followed_by C) . 1 = B & ( for n being Element of NAT st 1 < n holds
((A,B) followed_by C) . n = C ) ) by FUNCT_7:122, FUNCT_7:123, FUNCT_7:124, FUNCT_7:127; :: thesis: verum