deffunc H1( 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 = H1(d)
from FUNCT_2:sch 4();
take
f
; ( 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;
( k > 1 implies f . k = {1,2,3,4} --> 0 )
assume C1:
k > 1
;
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;
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; verum