let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module
for I being Basis of V
for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
let V be free Z_Module; :: thesis: for I being Basis of V
for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
let I be Basis of V; :: thesis: for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
let X be non empty Subset of (Z_MQ_VectSp (V,p)); :: thesis: ( X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I ) )
assume A1: X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
set ZQ = Z_MQ_VectSp (V,p);
defpred S₁[ Element of X, Element of V] means ( $2 in $1 & $2 in I );
A2: for x being Element of X ex v being Element of V st S₁[x,v]

proof

let x be Element of X; :: thesis: ex v being Element of V st S₁[x,v]
x in X ;
then consider v being Vector of V such that
A3: ( x = ZMtoMQV (V,p,v) & v in I ) by A1;
thus ex v being Element of V st S₁[x,v] by A3, ZMODUL01:58; :: thesis: verum

end;

consider F being Function of X, the carrier of V such that
A4: for x being Element of X holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
take F ; :: thesis: ( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )
thus for v being Vector of V st v in I holds
F . (ZMtoMQV (V,p,v)) = v :: thesis: ( F is one-to-one & dom F = X & rng F = I )

proof

let v be Vector of V; :: thesis: ( v in I implies F . (ZMtoMQV (V,p,v)) = v )
assume A5: v in I ; :: thesis: F . (ZMtoMQV (V,p,v)) = v
then ZMtoMQV (V,p,v) in X by A1;
then reconsider w = ZMtoMQV (V,p,v) as Element of X ;
A6: ( F . w in w & F . w in I ) by A4;
ZMtoMQV (V,p,(F . w)) = ZMtoMQV (V,p,v) by A4, ZMODUL01:67;
hence F . (ZMtoMQV (V,p,v)) = v by A5, A6, Th21; :: thesis: verum

end;

now :: thesis: for x1, x2 being object st x1 in X & x2 in X & F . x1 = F . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in X & x2 in X & F . x1 = F . x2 implies x1 = x2 )
assume A7: ( x1 in X & x2 in X & F . x1 = F . x2 ) ; :: thesis: x1 = x2
then reconsider x10 = x1, x20 = x2 as Element of X ;
consider v1 being Vector of V such that
A8: ( x1 = ZMtoMQV (V,p,v1) & v1 in I ) by A7, A1;
consider v2 being Vector of V such that
A9: ( x2 = ZMtoMQV (V,p,v2) & v2 in I ) by A7, A1;
( F . x10 in ZMtoMQV (V,p,v1) & F . x10 in ZMtoMQV (V,p,v2) ) by A7, A8, A9, A4;
then F . x10 in (ZMtoMQV (V,p,v1)) /\ (ZMtoMQV (V,p,v2)) by XBOOLE_0:def 4;
hence x1 = x2 by A8, A9, Lm2; :: thesis: verum

end;

hence F is one-to-one by FUNCT_2:19; :: thesis: ( dom F = X & rng F = I )
thus dom F = X by FUNCT_2:def 1; :: thesis: rng F = I

now :: thesis: for y being object st y in rng F holds
y in I

let y be object ; :: thesis: ( y in rng F implies y in I )
assume y in rng F ; :: thesis: y in I
then consider x being object such that
A10: ( x in X & F . x = y ) by FUNCT_2:11;
reconsider x = x as Element of X by A10;
thus y in I by A10, A4; :: thesis: verum

end;

then A11: rng F c= I ;

now :: thesis: for y being object st y in I holds
y in rng F

let y be object ; :: thesis: ( y in I implies y in rng F )
assume A12: y in I ; :: thesis: y in rng F
then reconsider u = y as Vector of V ;
ZMtoMQV (V,p,u) in X by A12, A1;
then reconsider z = ZMtoMQV (V,p,u) as Element of X ;
A13: ( F . z in z & F . z in I ) by A4;
ZMtoMQV (V,p,(F . z)) = ZMtoMQV (V,p,u) by A4, ZMODUL01:67;
then F . z = u by Th21, A13, A12;
hence y in rng F by FUNCT_2:4; :: thesis: verum

end;

then I c= rng F ;
hence I = rng F by A11, XBOOLE_0:def 10; :: thesis: verum