let AFV be strict AffVect; :: thesis: for o being Element of holds AFV = AV (GroupVect AFV,o)
let o be Element of ; :: 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 by A3, MCART_1:10;
reconsider x1' = x1, x2' = x2, y1' = y1, y2' = y2 as Element of ;
A6: x = [(x `1 ),(x `2 )] by A5, MCART_1:23;
then A7: x1,x2 // y1,y2 by A2, A4, ANALOAF:def 2;
x1' # y2' = x2' # y1'

proof

reconsider z1 = x1' # y2', z2 = x2' # y1' as Element of ;
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 x1' # y2' = x2' # y1' 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 x1' = x `1 , x2' = x `2 , y1' = y `1 , y2' = y `2 as Element of by A10, MCART_1:10;
set z1' = x1' # y2';
set z2' = x2' # y1';
reconsider x1 = x1', x2 = x2', y1 = y1', y2 = y2' as Element of ;
reconsider z1 = x1' # y2', z2 = x2' # y1' as Element of ;
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 x1' # y2' = x2' # y1' 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