let ADG be Proper_Uniquely_Two_Divisible_Group; :: thesis: for o' being Element of ADG
for o being Element of (AV ADG) st o = o' holds
ADG, GroupVect (AV ADG),o are_Iso
let o' be Element of ADG; :: thesis: for o being Element of (AV ADG) st o = o' holds
ADG, GroupVect (AV ADG),o are_Iso
let o be Element of (AV ADG); :: thesis: ( o = o' implies ADG, GroupVect (AV ADG),o are_Iso )
assume A1: o = o' ; :: thesis: ADG, GroupVect (AV ADG),o are_Iso
set AS = AV ADG;
set X = the carrier of ADG;
set Y = the carrier of (AV ADG);
set Z = GroupVect (AV ADG),o;
set T = the carrier of (GroupVect (AV ADG),o);
deffunc H₁( Element of the carrier of ADG) -> Element of the carrier of ADG = o' + $1;
consider g being UnOp of the carrier of ADG such that
A2: for a being Element of the carrier of ADG holds g . a = H₁(a) from FUNCT_2:sch 4();
( the carrier of ADG = the carrier of (GroupVect (AV ADG),o) & the carrier of ADG = the carrier of (AV ADG) & the carrier of (AV ADG) = the carrier of (GroupVect (AV ADG),o) ) by TDGROUP:9;
then reconsider f = g as Function of the carrier of ADG,the carrier of (GroupVect (AV ADG),o) ;
A3: f is one-to-one by A2, Th76;
A4: rng f = the carrier of (GroupVect (AV ADG),o) by A2, Th77;

now

let a, b be Element of ADG; :: thesis: ( f . (a + b) = (f . a) + (f . b) & f . (0. ADG) = 0. (GroupVect (AV ADG),o) & f . (- a) = - (f . a) )
thus f . (a + b) = (f . a) + (f . b) by A1, A2, Th75; :: thesis: ( f . (0. ADG) = 0. (GroupVect (AV ADG),o) & f . (- a) = - (f . a) )
thus f . (0. ADG) = 0. (GroupVect (AV ADG),o) by A1, A2, Th75; :: thesis: f . (- a) = - (f . a)
reconsider fa = f . a as Element of (AV ADG) ;
thus f . (- a) = (Pcom o) . fa by A1, A2, Th75
.= - (f . a) by Th58 ; :: thesis: verum

end;

then f is_Iso_of ADG, GroupVect (AV ADG),o by A3, A4, Def10;
hence ADG, GroupVect (AV ADG),o are_Iso by Def11; :: thesis: verum