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 () = n & idseq n is FinSequence of NAT ) by ;
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 ;
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 ;
then A4: rng IDnP c= dom A by ;
A5: ( IDn = Sgm (Seg n) & card (Seg n) = n ) by ;
then A6: Segm (A,IDnP,(Sgm (Seg ()))) = (Segm (A,(Seg (len A)),(Seg ()))) * P by
.= A * P by MATRIX13:46 ;
A7: len B = n by MATRIX_0:def 2;
then A8: Segm (B,IDnP,(Sgm (Seg ()))) = (Segm (B,(Seg (len B)),(Seg ()))) * P by
.= B * P by MATRIX13:46 ;
per cases ( n > 0 or n = 0 ) ;
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 ;
A12: dom B = Seg n by ;
assume P is one-to-one ; :: thesis: Solutions_of (A,B) = Solutions_of ((A * P),(B * P))
then P is onto by ;
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) = () |-> (0. K) & Line (B,i) = () |-> (0. K) ) by ;
hence Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) by A1, A3, A6, A8, A9, A11, A12, Th43; :: thesis: verum
end;
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 ;
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 ; :: thesis: verum
end;
end;