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