let F be Field; :: thesis: ( Char F <> 2 implies for a being Element of F holds (((a + (1. F)) / (2 '*' (1. F))) ^2) - (((a - (1. F)) / (2 '*' (1. F))) ^2) = a )
assume AS: Char F <> 2 ; :: thesis: for a being Element of F holds (((a + (1. F)) / (2 '*' (1. F))) ^2) - (((a - (1. F)) / (2 '*' (1. F))) ^2) = a
let a be Element of F; :: thesis: (((a + (1. F)) / (2 '*' (1. F))) ^2) - (((a - (1. F)) / (2 '*' (1. F))) ^2) = a
2 '*' (1. F) <> 0. F by AS, P5b;
then A1: (2 '*' (1. F)) * (2 '*' (1. F)) <> 0. F by VECTSP_1:12;
then C: (2 * 2) '*' (1. F) <> 0. F by RING_3:67;
D: not 2 '*' (1. F) is zero by AS, P5b;
thus (((a + (1. F)) / (2 '*' (1. F))) ^2) - (((a - (1. F)) / (2 '*' (1. F))) ^2) = (((a + (1. F)) ^2) / ((2 '*' (1. F)) ^2)) - (((a - (1. F)) / (2 '*' (1. F))) ^2) by D, P5a
.= (((a + (1. F)) ^2) / ((2 '*' (1. F)) ^2)) - (((a - (1. F)) ^2) / ((2 '*' (1. F)) ^2)) by D, P5a
.= (((a + (1. F)) ^2) - ((a - (1. F)) ^2)) / ((2 '*' (1. F)) ^2) by A1, VECTSP_2:20
.= ((((a ^2) + ((2 '*' a) * (1. F))) + ((1. F) ^2)) - ((a - (1. F)) ^2)) / ((2 '*' (1. F)) ^2) by P3
.= ((((a ^2) + (2 '*' a)) + ((1. F) ^2)) - (((a ^2) - ((2 '*' a) * (1. F))) + ((1. F) ^2))) / ((2 '*' (1. F)) ^2) by P4
.= ((((a ^2) + (2 '*' a)) + ((1. F) ^2)) + ((- ((a ^2) + (- (2 '*' a)))) + (- ((1. F) ^2)))) / ((2 '*' (1. F)) ^2) by RLVECT_1:31
.= ((((a ^2) + (2 '*' a)) + ((1. F) ^2)) + (((- (a ^2)) + (- (- (2 '*' a)))) + (- ((1. F) ^2)))) / ((2 '*' (1. F)) ^2) by RLVECT_1:31
.= (((a ^2) + (2 '*' a)) + (((1. F) ^2) + ((- ((1. F) ^2)) + ((- (a ^2)) + (2 '*' a))))) / ((2 '*' (1. F)) ^2) by RLVECT_1:def 3
.= (((a ^2) + (2 '*' a)) + ((((1. F) ^2) + (- ((1. F) ^2))) + ((- (a ^2)) + (2 '*' a)))) / ((2 '*' (1. F)) ^2) by RLVECT_1:def 3
.= (((a ^2) + (2 '*' a)) + ((0. F) + ((- (a ^2)) + (2 '*' a)))) / ((2 '*' (1. F)) ^2) by RLVECT_1:5
.= ((2 '*' a) + ((a ^2) + ((- (a ^2)) + (2 '*' a)))) / ((2 '*' (1. F)) ^2) by RLVECT_1:def 3
.= ((2 '*' a) + (((a ^2) + (- (a ^2))) + (2 '*' a))) / ((2 '*' (1. F)) ^2) by RLVECT_1:def 3
.= ((2 '*' a) + ((0. F) + (2 '*' a))) / ((2 '*' (1. F)) ^2) by RLVECT_1:5
.= ((2 + 2) '*' a) / ((2 '*' (1. F)) ^2) by RING_3:62
.= (4 '*' a) / ((2 * 2) '*' (1. F)) by RING_3:67
.= (4 '*' ((1. F) * a)) / (4 '*' (1. F))
.= ((4 '*' (1. F)) * a) / (4 '*' (1. F)) by c1
.= a / ((4 '*' (1. F)) / (4 '*' (1. F))) by C, VECTSP_2:21
.= a / (1_ F) by C, VECTSP_2:17
.= a ; :: thesis: verum