deffunc H₁( Nat) -> Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) = IFEQ ($1,0,(RVfirst 1),(IFEQ ($1,1,(RVfirst 5),(RVfirst 0))));
consider f being sequence of (set_of_random_variables_on (Special_SigmaField1,Borel_Sets)) such that
A1: for d being Element of NAT holds f . d = H₁(d) from FUNCT_2:sch 4();
take f ; :: thesis: ( f . 0 = {1,2,3,4} --> 1 & f . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
f . k = {1,2,3,4} --> 0 ) )
b1: f . 0 = IFEQ (0,0,(RVfirst 1),(IFEQ (0,1,(RVfirst 5),(RVfirst 0)))) by A1;
f . 1 = IFEQ (1,0,(RVfirst 1),(IFEQ (1,1,(RVfirst 5),(RVfirst 0)))) by A1;
then b2: f . 1 = IFEQ (1,1,(RVfirst 5),(RVfirst 0)) by FUNCOP_1:def 8;
for k being Nat st k > 1 holds
f . k = {1,2,3,4} --> 0

proof

let k be Nat; :: thesis: ( k > 1 implies f . k = {1,2,3,4} --> 0 )
assume C1: k > 1 ; :: thesis: f . k = {1,2,3,4} --> 0
k in NAT by ORDINAL1:def 12;
then f . k = IFEQ (k,0,(RVfirst 1),(IFEQ (k,1,(RVfirst 5),(RVfirst 0)))) by A1;
then f . k = IFEQ (k,1,(RVfirst 5),(RVfirst 0)) by C1, FUNCOP_1:def 8;
hence f . k = {1,2,3,4} --> 0 by C1, FUNCOP_1:def 8; :: thesis: verum

end;

hence ( f . 0 = {1,2,3,4} --> 1 & f . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
f . k = {1,2,3,4} --> 0 ) ) by b1, b2, FUNCOP_1:def 8; :: thesis: verum