let f1, f2 be linear-transformation of (VectQuot (V,(ker T))),(im T); :: thesis: ( f1 is bijective & ( for v being Element of V holds f1 . ((ZQMorph (V,(ker T))) . v) = T . v ) & f2 is bijective & ( for v being Element of V holds f2 . ((ZQMorph (V,(ker T))) . v) = T . v ) implies f1 = f2 )
assume AS1: ( f1 is one-to-one & f1 is onto & ( for v being Element of V holds f1 . ((ZQMorph (V,(ker T))) . v) = T . v ) ) ; :: according to FUNCT_2:def 4 :: thesis: ( not f2 is bijective or ex v being Element of V st not f2 . ((ZQMorph (V,(ker T))) . v) = T . v or f1 = f2 )
assume AS2: ( f2 is one-to-one & f2 is onto & ( for v being Element of V holds f2 . ((ZQMorph (V,(ker T))) . v) = T . v ) ) ; :: according to FUNCT_2:def 4 :: thesis: f1 = f2
YY: rng (ZQMorph (V,(ker T))) = the carrier of (VectQuot (V,(ker T))) by FUNCT_2:def 3;
for v being Element of (VectQuot (V,(ker T))) holds f1 . v = f2 . v

proof

let v be Element of (VectQuot (V,(ker T))); :: thesis: f1 . v = f2 . v
consider z being Element of V such that
A12: v = (ZQMorph (V,(ker T))) . z by FUNCT_2:113, YY;
thus f1 . v = T . z by A12, AS1
.= f2 . v by A12, AS2 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:def 8; :: thesis: verum