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

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

A1: now

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 by MCART_1:7;
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:23;
[x,y] `1 = x by MCART_1:7;
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:23;
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 Def7;
then o,x1 // y2,z1 by Def5;
then x1,o // z1,y2 by Th8;
then A8: o,x2 // y1,z1 by A7, Th13;
z2 = Padd o,x2,y1 by Def7;
hence x19 # y29 = x29 # y19 by A8, Def5; :: thesis: verum

end;

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

end;

now

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 by MCART_1:7;
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:23;
[x,y] `1 = x by MCART_1:7;
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 Def7;
z1 = Padd o,x1,y2 by Def7;
then A14: o,x1 // y2,z1 by Def5;
A15: x = [(x `1 ),(x `2 )] by A12, MCART_1:23;
then x19 # y29 = x29 # y19 by A9, A11, TDGROUP:def 4;
then o,x2 // y1,z1 by A13, Def5;
then x1,x2 // y1,y2 by A14, Th13;
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:9;
hence AFV = AV (GroupVect AFV,o) by TDGROUP:9; :: thesis: verum