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