let X be set ; :: thesis: for A1 being SetSequence of X ex B1 being SetSequence of X st
for n being Element of NAT holds B1 . n = (A1 . n) `
let A1 be SetSequence of X; :: thesis: ex B1 being SetSequence of X st
for n being Element of NAT holds B1 . n = (A1 . n) `
deffunc H₁( Element of NAT ) -> Event of = (A1 . $1) ` ;
ex f being Function of NAT ,(bool X) st
for x being Element of NAT holds f . x = H<sub>1</sub>(x) from FUNCT_2:sch 4();
then consider f being Function of NAT ,(bool X) such that
A1: for x being Element of NAT holds f . x = (A1 . x) ` ;
take f ; :: thesis: for n being Element of NAT holds f . n = (A1 . n) `
thus for n being Element of NAT holds f . n = (A1 . n) ` by A1; :: thesis: verum