let k, m, n be Nat; :: thesis: for K being Field

for A being Matrix of n,m,K

for B being Matrix of n,k,K

for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

let K be Field; :: thesis: for A being Matrix of n,m,K

for B being Matrix of n,k,K

for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

set IDn = idseq n;

( len (idseq n) = n & idseq n is FinSequence of NAT ) by CARD_1:def 7, FINSEQ_2:48;

then reconsider IDn = idseq n as Element of n -tuples_on NAT by FINSEQ_2:92;

let A be Matrix of n,m,K; :: thesis: for B being Matrix of n,k,K

for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

let B be Matrix of n,k,K; :: thesis: for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

let P be Function of (Seg n),(Seg n); :: thesis: ( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

A1: rng P c= Seg n by RELAT_1:def 19;

dom IDn = Seg n ;

then reconsider IDnP = IDn * P as FinSequence of NAT by FINSEQ_2:47;

dom P = Seg n by FUNCT_2:52;

then ( n in NAT & dom IDnP = Seg n ) by A1, ORDINAL1:def 12, RELAT_1:53;

then len IDnP = n by FINSEQ_1:def 3;

then reconsider IDnP = IDnP as Element of n -tuples_on NAT by FINSEQ_2:92;

A2: n = len A by MATRIX_0:def 2;

A3: (idseq n) * P = P by A1, RELAT_1:53;

then A4: rng IDnP c= dom A by A1, A2, FINSEQ_1:def 3;

A5: ( IDn = Sgm (Seg n) & card (Seg n) = n ) by FINSEQ_1:57, FINSEQ_3:48;

then A6: Segm (A,IDnP,(Sgm (Seg (width A)))) = (Segm (A,(Seg (len A)),(Seg (width A)))) * P by A2, MATRIX13:33

.= A * P by MATRIX13:46 ;

A7: len B = n by MATRIX_0:def 2;

then A8: Segm (B,IDnP,(Sgm (Seg (width B)))) = (Segm (B,(Seg (len B)),(Seg (width B)))) * P by A5, MATRIX13:33

.= B * P by MATRIX13:46 ;

for A being Matrix of n,m,K

for B being Matrix of n,k,K

for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

let K be Field; :: thesis: for A being Matrix of n,m,K

for B being Matrix of n,k,K

for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

set IDn = idseq n;

( len (idseq n) = n & idseq n is FinSequence of NAT ) by CARD_1:def 7, FINSEQ_2:48;

then reconsider IDn = idseq n as Element of n -tuples_on NAT by FINSEQ_2:92;

let A be Matrix of n,m,K; :: thesis: for B being Matrix of n,k,K

for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

let B be Matrix of n,k,K; :: thesis: for P being Function of (Seg n),(Seg n) holds

( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

let P be Function of (Seg n),(Seg n); :: thesis: ( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

A1: rng P c= Seg n by RELAT_1:def 19;

dom IDn = Seg n ;

then reconsider IDnP = IDn * P as FinSequence of NAT by FINSEQ_2:47;

dom P = Seg n by FUNCT_2:52;

then ( n in NAT & dom IDnP = Seg n ) by A1, ORDINAL1:def 12, RELAT_1:53;

then len IDnP = n by FINSEQ_1:def 3;

then reconsider IDnP = IDnP as Element of n -tuples_on NAT by FINSEQ_2:92;

A2: n = len A by MATRIX_0:def 2;

A3: (idseq n) * P = P by A1, RELAT_1:53;

then A4: rng IDnP c= dom A by A1, A2, FINSEQ_1:def 3;

A5: ( IDn = Sgm (Seg n) & card (Seg n) = n ) by FINSEQ_1:57, FINSEQ_3:48;

then A6: Segm (A,IDnP,(Sgm (Seg (width A)))) = (Segm (A,(Seg (len A)),(Seg (width A)))) * P by A2, MATRIX13:33

.= A * P by MATRIX13:46 ;

A7: len B = n by MATRIX_0:def 2;

then A8: Segm (B,IDnP,(Sgm (Seg (width B)))) = (Segm (B,(Seg (len B)),(Seg (width B)))) * P by A5, MATRIX13:33

.= B * P by MATRIX13:46 ;

per cases
( n > 0 or n = 0 )
;

end;

suppose A9:
n > 0
; :: thesis: ( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

hence
Solutions_of (A,B) c= Solutions_of ((A * P),(B * P))
by A6, A8, A4, Th42; :: thesis: ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) )

A10: card (Seg n) = card (Seg n) ;

A11: dom A = Seg n by A2, FINSEQ_1:def 3;

A12: dom B = Seg n by A7, FINSEQ_1:def 3;

assume P is one-to-one ; :: thesis: Solutions_of (A,B) = Solutions_of ((A * P),(B * P))

then P is onto by A10, STIRL2_1:60;

then rng P = Seg n by FUNCT_2:def 3;

then for i being Nat st i in (dom A) \ (rng IDnP) holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) by A3, A11, XBOOLE_1:37;

hence Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) by A1, A3, A6, A8, A9, A11, A12, Th43; :: thesis: verum

end;A10: card (Seg n) = card (Seg n) ;

A11: dom A = Seg n by A2, FINSEQ_1:def 3;

A12: dom B = Seg n by A7, FINSEQ_1:def 3;

assume P is one-to-one ; :: thesis: Solutions_of (A,B) = Solutions_of ((A * P),(B * P))

then P is onto by A10, STIRL2_1:60;

then rng P = Seg n by FUNCT_2:def 3;

then for i being Nat st i in (dom A) \ (rng IDnP) holds

( Line (A,i) = (width A) |-> (0. K) & Line (B,i) = (width B) |-> (0. K) ) by A3, A11, XBOOLE_1:37;

hence Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) by A1, A3, A6, A8, A9, A11, A12, Th43; :: thesis: verum

suppose A13:
n = 0
; :: thesis: ( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )

then
len B = 0
by MATRIX_0:22;

then A14: B = {} ;

len A = 0 by A13, MATRIX_0:22;

then A15: A = {} ;

A * P = {} by A13;

hence ( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) ) by A15, A14; :: thesis: verum

end;then A14: B = {} ;

len A = 0 by A13, MATRIX_0:22;

then A15: A = {} ;

A * P = {} by A13;

hence ( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) & ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) ) by A15, A14; :: thesis: verum