deffunc H₁( Nat) -> Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) = RVswitchfirst $1;
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 = RVswitchfirst 0 by A1;
f . 1 = RVswitchfirst 1 by A1;
then b2: f . 1 = RVswitchsecond 1 by Def60;
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 = RVswitchfirst k by A1;
then f . k = RVswitchsecond k by C1, Def60;
hence f . k = {1,2,3,4} --> 0 by C1, Def61; :: 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, Def61, Def60; :: thesis: verum