set x = [0,1];
set x1 = [0,0];
set p1 = [0,0] .--> [0,0,1];
set p2 = [0,1] .--> [1,0,1];
set p3 = [1,1] .--> [1,1,1];
set p4 = [1,0] .--> [2,1,1];
set p5 = [2,1] .--> [2,1,1];
set p6 = [2,0] .--> [3,0,(- 1)];
set p7 = [3,1] .--> [4,0,(- 1)];
set p8 = [4,1] .--> [4,1,(- 1)];
set f = id ([:(SegM 5),{0,1}:],{(- 1),0,1},0);
thus Sum_Tran . [0,0] = (((((((((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)])) . [0,0] by Th2
.= ((((((((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)])) . [0,0] by Th2
.= (((((((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)])) . [0,0] by Th2
.= ((((((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])) . [0,0] by Th2
.= (((((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])) . [0,0] by Th2
.= ((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) . [0,0] by Th2
.= (((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) . [0,0] by Th2
.= ((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) . [0,0] by Th3
.= [0,0,1] by FUNCT_7:94 ; :: thesis: ( Sum_Tran . [0,1] = [1,0,1] & Sum_Tran . [1,1] = [1,1,1] & Sum_Tran . [1,0] = [2,1,1] & Sum_Tran . [2,1] = [2,1,1] & Sum_Tran . [2,0] = [3,0,(- 1)] & Sum_Tran . [3,1] = [4,0,(- 1)] & Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )
thus Sum_Tran . [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)])) . [0,1] by Th2
.= ((((((((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)])) . [0,1] by Th2
.= (((((((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)])) . [0,1] by Th2
.= ((((((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])) . [0,1] by Th2
.= (((((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])) . [0,1] by Th2
.= ((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) . [0,1] by Th2
.= (((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) . [0,1] by Th2
.= [1,0,1] by FUNCT_7:94 ; :: thesis: ( Sum_Tran . [1,1] = [1,1,1] & Sum_Tran . [1,0] = [2,1,1] & Sum_Tran . [2,1] = [2,1,1] & Sum_Tran . [2,0] = [3,0,(- 1)] & Sum_Tran . [3,1] = [4,0,(- 1)] & Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )
set x = [1,1];
thus Sum_Tran . [1,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)])) . [1,1] by Th2
.= ((((((((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)])) . [1,1] by Th2
.= (((((((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)])) . [1,1] by Th2
.= ((((((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])) . [1,1] by Th2
.= (((((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])) . [1,1] by Th2
.= ((((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,1] by Th3
.= [1,1,1] by FUNCT_7:94 ; :: thesis: ( Sum_Tran . [1,0] = [2,1,1] & Sum_Tran . [2,1] = [2,1,1] & Sum_Tran . [2,0] = [3,0,(- 1)] & Sum_Tran . [3,1] = [4,0,(- 1)] & Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )
set x = [1,0];
thus Sum_Tran . [1,0] = (((((((((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)])) . [1,0] by Th2
.= ((((((((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)])) . [1,0] by Th2
.= (((((((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)])) . [1,0] by Th2
.= ((((((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])) . [1,0] by Th2
.= (((((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])) . [1,0] by Th2
.= [2,1,1] by FUNCT_7:94 ; :: thesis: ( Sum_Tran . [2,1] = [2,1,1] & Sum_Tran . [2,0] = [3,0,(- 1)] & Sum_Tran . [3,1] = [4,0,(- 1)] & Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )
set x = [2,1];
thus Sum_Tran . [2,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)])) . [2,1] by Th2
.= ((((((((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)])) . [2,1] by Th2
.= (((((((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)])) . [2,1] by Th2
.= ((((((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,1] by Th3
.= [2,1,1] by FUNCT_7:94 ; :: thesis: ( Sum_Tran . [2,0] = [3,0,(- 1)] & Sum_Tran . [3,1] = [4,0,(- 1)] & Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )
set x = [2,0];
thus Sum_Tran . [2,0] = (((((((((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)])) . [2,0] by Th2
.= ((((((((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)])) . [2,0] by Th2
.= (((((((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)])) . [2,0] by Th2
.= [3,0,(- 1)] by FUNCT_7:94 ; :: thesis: ( Sum_Tran . [3,1] = [4,0,(- 1)] & Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )
set x = [3,1];
thus Sum_Tran . [3,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)])) . [3,1] by Th2
.= ((((((((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)])) . [3,1] by Th2
.= [4,0,(- 1)] by FUNCT_7:94 ; :: thesis: ( Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )
set x = [4,1];
thus Sum_Tran . [4,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,1] by Th3
.= [4,1,(- 1)] by FUNCT_7:94 ; :: thesis: Sum_Tran . [4,0] = [5,0,0]
thus Sum_Tran . [4,0] = [5,0,0] by FUNCT_7:94; :: thesis: verum