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: [.b,(c " ),a.] = ([.b,(c " ).] " ) * (((a " ) * [.b,(c " ).]) * a) by Th19
.= [.(c " ),b.] * (((a " ) * [.b,(c " ).]) * a) by Th25 ;
[.(c " ),b.] = ((c " ) " ) * (((b " ) * (c " )) * b) by Th19;
then A2: [.b,(c " ),a.] |^ c = ((c " ) * (((c " ) " ) * ((((b " ) * (c " )) * b) * (((a " ) * [.b,(c " ).]) * a)))) * c by A1, GROUP_1:def 4
.= ((((b " ) * (c " )) * b) * (((a " ) * [.b,(c " ).]) * a)) * c by GROUP_3:1
.= (((b " ) * (c " )) * b) * ((((a " ) * [.b,(c " ).]) * a) * c) by GROUP_1:def 4
.= ((b " ) * ((c " ) * b)) * ((((a " ) * [.b,(c " ).]) * a) * c) by GROUP_1:def 4
.= (b " ) * (((c " ) * b) * ((((a " ) * [.b,(c " ).]) * a) * c)) by GROUP_1:def 4 ;
A3: [.c,(a " ),b.] = ([.c,(a " ).] " ) * (((b " ) * [.c,(a " ).]) * b) by Th19
.= [.(a " ),c.] * (((b " ) * [.c,(a " ).]) * b) by Th25 ;
A4: [.(a " ),c.] = ((a " ) " ) * (((c " ) * (a " )) * c) by Th19;
A5: [.a,(b " ),c.] = ([.a,(b " ).] " ) * (((c " ) * [.a,(b " ).]) * c) by Th19
.= [.(b " ),a.] * (((c " ) * [.a,(b " ).]) * c) by Th25 ;
A6: [.(b " ),a.] = ((b " ) " ) * (((a " ) * (b " )) * a) by Th19;
A7: [.c,(a " ),b.] |^ a = ((a " ) * (((a " ) " ) * ((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)))) * a by A3, A4, GROUP_1:def 4
.= ((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a by GROUP_3:1 ;
[.a,(b " ),c.] |^ b = ((b " ) * (((b " ) " ) * ((((a " ) * (b " )) * a) * (((c " ) * [.a,(b " ).]) * c)))) * b by A5, A6, GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * (((c " ) * [.a,(b " ).]) * c)) * b by GROUP_3:1 ;
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 A2, GROUP_1:def 4
.= ((((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 4
.= (((((a " ) * (b " )) * a) * (c " )) * ([.a,(b " ).] * c)) * (((c " ) * b) * ((((a " ) * [.b,(c " ).]) * a) * c)) by GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * (c " )) * (([.a,(b " ).] * c) * (((c " ) * b) * ((((a " ) * [.b,(c " ).]) * a) * c))) by GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * (c " )) * ((([.a,(b " ).] * c) * ((c " ) * b)) * ((((a " ) * [.b,(c " ).]) * a) * c)) by GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * (c " )) * (((([.a,(b " ).] * c) * (c " )) * b) * ((((a " ) * [.b,(c " ).]) * a) * c)) by GROUP_1:def 4
.= ((((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 4
.= ((((a " ) * (b " )) * a) * (c " )) * ((((a " ) * ((b " ) " )) * a) * ((a " ) * ([.b,(c " ).] * (a * c)))) by GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * (c " )) * (((((a " ) * ((b " ) " )) * a) * (a " )) * ([.b,(c " ).] * (a * c))) by GROUP_1:def 4
.= ((((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 4
.= ((((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 4
.= ((((a " ) * (b " )) * a) * (c " )) * (((a " ) * ((b " ) " )) * ((b " ) * (((((c " ) " ) * b) * (c " )) * (a * c)))) by GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * (c " )) * ((((a " ) * ((b " ) " )) * (b " )) * (((((c " ) " ) * b) * (c " )) * (a * c))) by GROUP_1:def 4
.= ((((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 A7, GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * ((c " ) * (((a " ) * ((((c " ) " ) * b) * (c " ))) * (a * c)))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * ((c " ) * ((a " ) * (((((c " ) " ) * b) * (c " )) * (a * c))))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= (((((a " ) * (b " )) * a) * (c " )) * ((a " ) * (((((c " ) " ) * b) * (c " )) * (a * c)))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= (((((a " ) * (b " )) * a) * (c " )) * ((a " ) * ((((c " ) " ) * (b * (c " ))) * (a * c)))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= (((((a " ) * (b " )) * a) * (c " )) * ((a " ) * (((c " ) " ) * ((b * (c " )) * (a * c))))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= ((((((a " ) * (b " )) * a) * (c " )) * (a " )) * (((c " ) " ) * ((b * (c " )) * (a * c)))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= (((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * ((b * (c " )) * (a * c))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= (((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * (b * ((c " ) * (a * c)))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * ((c " ) * (a * c))) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= (((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * (a * c)) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a) by GROUP_1:def 4
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * ((a * c) * (((((c " ) * (a " )) * c) * (((b " ) * [.c,(a " ).]) * b)) * a)) by GROUP_1:def 4
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * ((a * c) * ((((c " ) * (a " )) * c) * ((((b " ) * [.c,(a " ).]) * b) * a))) by GROUP_1:def 4
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * ((a * c) * (((c " ) * (a " )) * (c * ((((b " ) * [.c,(a " ).]) * b) * a)))) by GROUP_1:def 4
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * (((a * c) * ((c " ) * (a " ))) * (c * ((((b " ) * [.c,(a " ).]) * b) * a))) by GROUP_1:def 4
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * (((a * c) * ((a * c) " )) * (c * ((((b " ) * [.c,(a " ).]) * b) * a))) by GROUP_1:25
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * ((1_ G) * (c * ((((b " ) * [.c,(a " ).]) * b) * a))) by GROUP_1:def 6
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * (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) * ((((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 4
.= (((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * ((b " ) * ([.c,(a " ).] * (b * a))) by GROUP_1:def 4
.= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (b " )) * ([.c,(a " ).] * (b * a)) by GROUP_1:def 4
.= ((((((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 4
.= (((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * (c " )) * (((((a " ) " ) * c) * (a " )) * (b * a)) by GROUP_1:def 4
.= (((((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 4
.= (((((a " ) * (b " )) * a) * (c " )) * (a " )) * (((a " ) " ) * ((c * (a " )) * (b * a))) by GROUP_1:def 4
.= ((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((a " ) " )) * ((c * (a " )) * (b * a)) by GROUP_1:def 4
.= ((((a " ) * (b " )) * a) * (c " )) * ((c * (a " )) * (b * a)) by GROUP_3:1
.= (((((a " ) * (b " )) * a) * (c " )) * (c * (a " ))) * (b * a) by GROUP_1:def 4
.= ((((a " ) * (b " )) * (a * (c " ))) * (c * (a " ))) * (b * a) by GROUP_1:def 4
.= ((((a " ) * (b " )) * (a * (c " ))) * (((c " ) " ) * (a " ))) * (b * a)
.= ((((a " ) * (b " )) * (a * (c " ))) * ((a * (c " )) " )) * (b * a) by GROUP_1:25
.= (((a " ) * (b " )) * ((a * (c " )) * ((a * (c " )) " ))) * (b * a) by GROUP_1:def 4
.= (((a " ) * (b " )) * (1_ G)) * (b * a) by GROUP_1:def 6
.= ((a " ) * (b " )) * (b * a) by GROUP_1:def 5
.= ((b * a) " ) * (b * a) by GROUP_1:25 ;
hence (([.a,(b " ),c.] |^ b) * ([.b,(c " ),a.] |^ c)) * ([.c,(a " ),b.] |^ a) = 1_ G by GROUP_1:def 6; :: thesis: verum