let ADG be Proper_Uniquely_Two_Divisible_Group; :: thesis: for o9 being Element of ADG
for o being Element of (AV ADG) st o = o9 holds
ADG, GroupVect ((AV ADG),o) are_Iso
let o9 be Element of ADG; :: thesis: for o being Element of (AV ADG) st o = o9 holds
ADG, GroupVect ((AV ADG),o) are_Iso
let o be Element of (AV ADG); :: thesis: ( o = o9 implies ADG, GroupVect ((AV ADG),o) are_Iso )
assume A1: o = o9 ; :: thesis: ADG, GroupVect ((AV ADG),o) are_Iso
set AS = AV ADG;
set X = the carrier of 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 = o9 + $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)) by TDGROUP:4;
then reconsider f = g as Function of the carrier of ADG, the carrier of (GroupVect ((AV ADG),o)) ;

A3: now :: thesis: for a, b being Element of ADG holds
( f . (a + b) = (f . a) + (f . b) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = - (f . a) )

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) )
reconsider fa = f . a as Element of (AV ADG) ;
thus f . (a + b) = (f . a) + (f . b) by A1, A2, Th52; :: 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, Th52; :: thesis: f . (- a) = - (f . a)
thus f . (- a) = (Pcom o) . fa by A1, A2, Th52
.= - (f . a) by Th44 ; :: thesis: verum

end;

( f is one-to-one & rng f = the carrier of (GroupVect ((AV ADG),o)) ) by A2, Th53, Th54;
then f is_Iso_of ADG, GroupVect ((AV ADG),o) by A3;
hence ADG, GroupVect ((AV ADG),o) are_Iso ; :: thesis: verum