let AFV be strict AffVect; :: thesis: for o being Element of AFV holds AFV = AV (GroupVect (AFV,o))
let o be Element of AFV; :: thesis: AFV = AV (GroupVect (AFV,o))
set X = GroupVect (AFV,o);

now :: thesis: for x, y being object holds
( [x,y] in CONGRD (GroupVect (AFV,o)) iff [x,y] in the CONGR of AFV )

let x, y be object ; :: thesis: ( [x,y] in CONGRD (GroupVect (AFV,o)) iff [x,y] in the CONGR of AFV )
set xy = [x,y];

A1: now :: thesis: ( [x,y] in the CONGR of AFV implies [x,y] in CONGRD (GroupVect (AFV,o)) )

set V = the carrier of AFV;
assume A2: [x,y] in the CONGR of AFV ; :: thesis: [x,y] in CONGRD (GroupVect (AFV,o))
set VV = [: the carrier of AFV, the carrier of AFV:];
[x,y] `2 = y ;
then A3: y in [: the carrier of AFV, the carrier of AFV:] by A2, MCART_1:10;
then A4: y = [(y `1),(y `2)] by MCART_1:21;
[x,y] `1 = x ;
then A5: x in [: the carrier of AFV, the carrier of AFV:] by A2, MCART_1:10;
then reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of AFV by A3, MCART_1:10;
reconsider x19 = x1, x29 = x2, y19 = y1, y29 = y2 as Element of (GroupVect (AFV,o)) ;
A6: x = [(x `1),(x `2)] by A5, MCART_1:21;
then A7: x1,x2 // y1,y2 by A2, A4, ANALOAF:def 2;
x19 # y29 = x29 # y19

proof

reconsider z1 = x19 # y29, z2 = x29 # y19 as Element of AFV ;
z1 = Padd (o,x1,y2) by Def6;
then o,x1 // y2,z1 by Def5;
then x1,o // z1,y2 by Th7;
then A8: o,x2 // y1,z1 by A7, Th12;
z2 = Padd (o,x2,y1) by Def6;
hence x19 # y29 = x29 # y19 by A8, Def5; :: thesis: verum

end;

hence [x,y] in CONGRD (GroupVect (AFV,o)) by A6, A4, TDGROUP:def 2; :: thesis: verum

end;

now :: thesis: ( [x,y] in CONGRD (GroupVect (AFV,o)) implies [x,y] in the CONGR of AFV )

set V = the carrier of (GroupVect (AFV,o));
assume A9: [x,y] in CONGRD (GroupVect (AFV,o)) ; :: thesis: [x,y] in the CONGR of AFV
set VV = [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):];
[x,y] `2 = y ;
then A10: y in [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):] by A9, MCART_1:10;
then A11: y = [(y `1),(y `2)] by MCART_1:21;
[x,y] `1 = x ;
then A12: x in [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):] by A9, MCART_1:10;
then reconsider x19 = x `1 , x29 = x `2 , y19 = y `1 , y29 = y `2 as Element of (GroupVect (AFV,o)) by A10, MCART_1:10;
set z19 = x19 # y29;
set z29 = x29 # y19;
reconsider x1 = x19, x2 = x29, y1 = y19, y2 = y29 as Element of AFV ;
reconsider z1 = x19 # y29, z2 = x29 # y19 as Element of AFV ;
A13: z2 = Padd (o,x2,y1) by Def6;
z1 = Padd (o,x1,y2) by Def6;
then A14: o,x1 // y2,z1 by Def5;
A15: x = [(x `1),(x `2)] by A12, MCART_1:21;
then x19 # y29 = x29 # y19 by A9, A11, TDGROUP:def 2;
then o,x2 // y1,z1 by A13, Def5;
then x1,x2 // y1,y2 by A14, Th12;
hence [x,y] in the CONGR of AFV by A15, A11, ANALOAF:def 2; :: thesis: verum

end;

hence ( [x,y] in CONGRD (GroupVect (AFV,o)) iff [x,y] in the CONGR of AFV ) by A1; :: thesis: verum

end;

then ( the carrier of (AV (GroupVect (AFV,o))) = the carrier of AFV & CONGRD (GroupVect (AFV,o)) = the CONGR of AFV ) by RELAT_1:def 2, TDGROUP:4;
hence AFV = AV (GroupVect (AFV,o)) by TDGROUP:4; :: thesis: verum