reconsider p0 = 0 , p1 = 1, p2 = 2, p3 = 3, p4 = 4, p5 = 5 as Element of SegM 5 by Th1;
set A = [:(SegM 5),{0,1}:];
set B = {(- 1),0,1};
set C = [:(SegM 5),{0,1},{(- 1),0,1}:];
reconsider b0 = 0 , b1 = 1 as Element of {0,1} by TARSKI:def 2;
reconsider L = - 1 as Element of {(- 1),0,1} by ENUMSET1:def 1;
reconsider h = 0 , R = 1 as Element of {(- 1),0,1} by ENUMSET1:def 1;
[:(SegM 5),{0,1},{(- 1),0,1}:] = [:[:(SegM 5),{0,1}:],{(- 1),0,1}:] by ZFMISC_1:def 3;
then reconsider OP = id ([:(SegM 5),{0,1}:],{(- 1),0,1},h) as Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:] ;
(((((((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,0,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0] .--> [5,0,0]) = ((((((((OP +* ([p0,b0] .--> [p0,b0,R])) +* ([p0,b1] .--> [p1,b0,R])) +* ([p1,b1] .--> [p1,b1,R])) +* ([p1,b0] .--> [p2,b1,R])) +* ([p2,b1] .--> [p2,b1,R])) +* ([p2,b0] .--> [p3,b0,L])) +* ([p3,b1] .--> [p4,b0,L])) +* ([p4,b1] .--> [p4,b1,L])) +* ([p4,b0] .--> [p5,b0,h]) ;
hence (((((((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,0,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0] .--> [5,0,0]) is Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:] ; :: thesis: verum