let G be Group; :: thesis: 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; :: thesis: (([.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 Th16;
A2: [.(a "),c.] = ((a ") ") * (((c ") * (a ")) * c) by Th16;
A3: [.(b "),a.] = ((b ") ") * (((a ") * (b ")) * a) by Th16;
[.a,(b "),c.] = ([.a,(b ").] ") * (((c ") * [.a,(b ").]) * c) by Th16
.= [.(b "),a.] * (((c ") * [.a,(b ").]) * c) by Th22 ;
then A4: [.a,(b "),c.] |^ b = ((b ") * (((b ") ") * ((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)))) * b by
.= ((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)) * b by GROUP_3:1 ;
[.c,(a "),b.] = ([.c,(a ").] ") * (((b ") * [.c,(a ").]) * b) by Th16
.= [.(a "),c.] * (((b ") * [.c,(a ").]) * b) by Th22 ;
then A5: [.c,(a "),b.] |^ a = ((a ") * (((a ") ") * ((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)))) * a by
.= ((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a by GROUP_3:1 ;
[.b,(c "),a.] = ([.b,(c ").] ") * (((a ") * [.b,(c ").]) * a) by Th16
.= [.(c "),b.] * (((a ") * [.b,(c ").]) * a) by Th22 ;
then [.b,(c "),a.] |^ c = ((c ") * (((c ") ") * ((((b ") * (c ")) * b) * (((a ") * [.b,(c ").]) * a)))) * c by
.= ((((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
.= ((((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 Th16
.= ((((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
.= ((((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 Th16
.= ((((((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; :: thesis: verum