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_{1}[ 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_{1}[x,v]

A4: for x being Element of X holds S_{1}[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 )

thus dom F = X by FUNCT_2:def 1; :: thesis: rng F = I

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

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

A2: for x being Element of X ex v being Element of V st S

proof

consider F being Function of X, the carrier of V such that
let x be Element of X; :: thesis: ex v being Element of V st S_{1}[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_{1}[x,v]
by A3, ZMODUL01:58; :: thesis: verum

end;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

A4: for x being Element of X holds S

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;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

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

x1 = x2

hence
F is one-to-one
by FUNCT_2:19; :: thesis: ( dom F = X & rng F = I )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;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

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

then A11:
rng F c= I
;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;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

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

y in rng F

then
I c= rng F
;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;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

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