let G be Group; for a, b, c being Element of G holds (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G
let a, b, c be Element of G; (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G
set d = ((a ") * [.b,(c ").]) * a;
set e = ((c ") * [.a,(b ").]) * c;
set f = ((b ") * [.c,(a ").]) * b;
set x = [.a,(b "),c.] |^ b;
set y = [.b,(c "),a.] |^ c;
set z = [.c,(a "),b.] |^ a;
A1:
[.(c "),b.] = ((c ") ") * (((b ") * (c ")) * b)
by Th19;
A2:
[.(a "),c.] = ((a ") ") * (((c ") * (a ")) * c)
by Th19;
A3:
[.(b "),a.] = ((b ") ") * (((a ") * (b ")) * a)
by Th19;
[.a,(b "),c.] =
([.a,(b ").] ") * (((c ") * [.a,(b ").]) * c)
by Th19
.=
[.(b "),a.] * (((c ") * [.a,(b ").]) * c)
by Th25
;
then A4: [.a,(b "),c.] |^ b =
((b ") * (((b ") ") * ((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)))) * b
by A3, GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)) * b
by GROUP_3:1
;
[.c,(a "),b.] =
([.c,(a ").] ") * (((b ") * [.c,(a ").]) * b)
by Th19
.=
[.(a "),c.] * (((b ") * [.c,(a ").]) * b)
by Th25
;
then A5: [.c,(a "),b.] |^ a =
((a ") * (((a ") ") * ((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)))) * a
by A2, GROUP_1:def 3
.=
((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a
by GROUP_3:1
;
[.b,(c "),a.] =
([.b,(c ").] ") * (((a ") * [.b,(c ").]) * a)
by Th19
.=
[.(c "),b.] * (((a ") * [.b,(c ").]) * a)
by Th25
;
then [.b,(c "),a.] |^ c =
((c ") * (((c ") ") * ((((b ") * (c ")) * b) * (((a ") * [.b,(c ").]) * a)))) * c
by A1, GROUP_1:def 3
.=
((((b ") * (c ")) * b) * (((a ") * [.b,(c ").]) * a)) * c
by GROUP_3:1
.=
(((b ") * (c ")) * b) * ((((a ") * [.b,(c ").]) * a) * c)
by GROUP_1:def 3
.=
((b ") * ((c ") * b)) * ((((a ") * [.b,(c ").]) * a) * c)
by GROUP_1:def 3
.=
(b ") * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_1:def 3
;
then ([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c) =
((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)) * (b * ((b ") * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c))))
by A4, GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_3:1
.=
((((a ") * (b ")) * a) * ((c ") * ([.a,(b ").] * c))) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_1:def 3
.=
(((((a ") * (b ")) * a) * (c ")) * ([.a,(b ").] * c)) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * (([.a,(b ").] * c) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c)))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * ((([.a,(b ").] * c) * ((c ") * b)) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * (((([.a,(b ").] * c) * (c ")) * b) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * ((((((a ") * ((b ") ")) * a) * (b ")) * b) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_3:1
.=
((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * a) * ((((a ") * [.b,(c ").]) * a) * c))
by GROUP_3:1
.=
((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * a) * (((a ") * [.b,(c ").]) * (a * c)))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * a) * ((a ") * ([.b,(c ").] * (a * c))))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * (((((a ") * ((b ") ")) * a) * (a ")) * ([.b,(c ").] * (a * c)))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * (((a ") * ((b ") ")) * ([.b,(c ").] * (a * c)))
by GROUP_3:1
.=
((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * [.b,(c ").]) * (a * c))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * ((b ") * ((((c ") ") * b) * (c ")))) * (a * c))
by Th19
.=
((((a ") * (b ")) * a) * (c ")) * (((a ") * ((b ") ")) * (((b ") * ((((c ") ") * b) * (c "))) * (a * c)))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * (((a ") * ((b ") ")) * ((b ") * (((((c ") ") * b) * (c ")) * (a * c))))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * (b ")) * (((((c ") ") * b) * (c ")) * (a * c)))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * ((a ") * (((((c ") ") * b) * (c ")) * (a * c)))
by GROUP_3:1
;
then (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) =
(((((a ") * (b ")) * a) * (c ")) * (((a ") * ((((c ") ") * b) * (c "))) * (a * c))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by A5, GROUP_1:def 3
.=
((((a ") * (b ")) * a) * ((c ") * (((a ") * ((((c ") ") * b) * (c "))) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * ((c ") * ((a ") * (((((c ") ") * b) * (c ")) * (a * c))))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
(((((a ") * (b ")) * a) * (c ")) * ((a ") * (((((c ") ") * b) * (c ")) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
(((((a ") * (b ")) * a) * (c ")) * ((a ") * ((((c ") ") * (b * (c "))) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
(((((a ") * (b ")) * a) * (c ")) * ((a ") * (((c ") ") * ((b * (c ")) * (a * c))))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
((((((a ") * (b ")) * a) * (c ")) * (a ")) * (((c ") ") * ((b * (c ")) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
(((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * ((b * (c ")) * (a * c))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
(((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * (b * ((c ") * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * ((c ") * (a * c))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
(((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (a * c)) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)
by GROUP_1:def 3
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((a * c) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a))
by GROUP_1:def 3
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((a * c) * ((((c ") * (a ")) * c) * ((((b ") * [.c,(a ").]) * b) * a)))
by GROUP_1:def 3
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((a * c) * (((c ") * (a ")) * (c * ((((b ") * [.c,(a ").]) * b) * a))))
by GROUP_1:def 3
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (((a * c) * ((c ") * (a "))) * (c * ((((b ") * [.c,(a ").]) * b) * a)))
by GROUP_1:def 3
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (((a * c) * ((a * c) ")) * (c * ((((b ") * [.c,(a ").]) * b) * a)))
by GROUP_1:17
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((1_ G) * (c * ((((b ") * [.c,(a ").]) * b) * a)))
by GROUP_1:def 5
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (c * ((((b ") * [.c,(a ").]) * b) * a))
by GROUP_1:def 4
.=
(((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * c) * ((((b ") * [.c,(a ").]) * b) * a)
by GROUP_1:def 3
.=
(((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * ((((b ") * [.c,(a ").]) * b) * a)
by GROUP_3:1
.=
(((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (((b ") * [.c,(a ").]) * (b * a))
by GROUP_1:def 3
.=
(((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * ((b ") * ([.c,(a ").] * (b * a)))
by GROUP_1:def 3
.=
((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (b ")) * ([.c,(a ").] * (b * a))
by GROUP_1:def 3
.=
((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * ([.c,(a ").] * (b * a))
by GROUP_3:1
.=
((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * (((c ") * ((((a ") ") * c) * (a "))) * (b * a))
by Th19
.=
((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * ((c ") * (((((a ") ") * c) * (a ")) * (b * a)))
by GROUP_1:def 3
.=
(((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * (c ")) * (((((a ") ") * c) * (a ")) * (b * a))
by GROUP_1:def 3
.=
(((((a ") * (b ")) * a) * (c ")) * (a ")) * (((((a ") ") * c) * (a ")) * (b * a))
by GROUP_3:1
.=
(((((a ") * (b ")) * a) * (c ")) * (a ")) * ((((a ") ") * (c * (a "))) * (b * a))
by GROUP_1:def 3
.=
(((((a ") * (b ")) * a) * (c ")) * (a ")) * (((a ") ") * ((c * (a ")) * (b * a)))
by GROUP_1:def 3
.=
((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((a ") ")) * ((c * (a ")) * (b * a))
by GROUP_1:def 3
.=
((((a ") * (b ")) * a) * (c ")) * ((c * (a ")) * (b * a))
by GROUP_3:1
.=
(((((a ") * (b ")) * a) * (c ")) * (c * (a "))) * (b * a)
by GROUP_1:def 3
.=
((((a ") * (b ")) * (a * (c "))) * (c * (a "))) * (b * a)
by GROUP_1:def 3
.=
((((a ") * (b ")) * (a * (c "))) * (((c ") ") * (a "))) * (b * a)
.=
((((a ") * (b ")) * (a * (c "))) * ((a * (c ")) ")) * (b * a)
by GROUP_1:17
.=
(((a ") * (b ")) * ((a * (c ")) * ((a * (c ")) "))) * (b * a)
by GROUP_1:def 3
.=
(((a ") * (b ")) * (1_ G)) * (b * a)
by GROUP_1:def 5
.=
((a ") * (b ")) * (b * a)
by GROUP_1:def 4
.=
((b * a) ") * (b * a)
by GROUP_1:17
;
hence
(([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G
by GROUP_1:def 5; verum