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
; ( 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
; ( 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
; ( 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
; U3(n)Tran . [2,0] = [3,0,0]
thus
U3(n)Tran . [2,0] = [3,0,0]
by FUNCT_7:94; verum