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 S1[ 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 S1[x,v]
proof
let x be Element of X; :: thesis: ex v being Element of V st S1[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 S1[x,v] by ; :: thesis: verum
end;
consider F being Function of X, the carrier of V such that
A4: for x being Element of X holds S1[x,F . x] from 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 ;
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 ; :: 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 ;
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 ;
then F . z = u by ;
hence y in rng F by FUNCT_2:4; :: thesis: verum
end;
then I c= rng F ;
hence I = rng F by ; :: thesis: verum