let n, m be Nat; :: thesis: for D being non empty set
for A, B being Matrix of n,m,D
for i being Nat st i <= n & 0 < n holds
for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
let D be non empty set ; :: thesis: for A, B being Matrix of n,m,D
for i being Nat st i <= n & 0 < n holds
for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
let A, B be Matrix of n,m,D; :: thesis: for i being Nat st i <= n & 0 < n holds
for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
let i be Nat; :: thesis: ( i <= n & 0 < n implies for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) ) )
assume A1: ( i <= n & 0 < n ) ; :: thesis: for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
let F be Function of (Seg i),(Seg n); :: thesis: ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
set I = idseq n;
set IF = (idseq n) +* F;
A2: ( i <= n & dom F = Seg i ) by A1, FUNCT_2:def 1;
then ( rng F c= Seg n & dom F c= Seg n ) by FINSEQ_1:7, RELAT_1:def 19;
then ( (rng F) \/ (Seg n) = Seg n & (dom F) \/ (Seg n) = Seg n & dom (idseq n) = Seg n & rng (idseq n) = Seg n ) by RELAT_1:71, XBOOLE_1:12;
then ( rng ((idseq n) +* F) c= Seg n & dom ((idseq n) +* F) = Seg n ) by FUNCT_4:18, FUNCT_4:def 1;
then reconsider IF = (idseq n) +* F as Function of (Seg n),(Seg n) by FUNCT_2:4;
reconsider BIF = B * IF as Matrix of n,m,D ;
set BIFi = BIF | (Seg i);
set M = A +* (BIF | (Seg i));
( len BIF = len B & len B = n ) by A1, Def4, MATRIX_1:24;
then ( dom BIF = Seg n & Seg i c= Seg n & len A = n ) by A1, FINSEQ_1:7, FINSEQ_1:def 3, MATRIX_1:24;
then A3: ( dom (BIF | (Seg i)) = Seg i & Seg i c= dom A & dom A = Seg n ) by FINSEQ_1:def 3, RELAT_1:91;
then A4: ( dom (A +* (BIF | (Seg i))) = (Seg i) \/ (Seg n) & (Seg i) \/ (Seg n) = Seg n & n is Element of NAT ) by FUNCT_4:def 1, ORDINAL1:def 13, XBOOLE_1:12;
then reconsider M = A +* (BIF | (Seg i)) as FinSequence by FINSEQ_1:def 2;
A5: for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) )

proof

let j be Nat; :: thesis: ( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) )
thus ( j in Seg i implies M . j = B . (F . j) ) :: thesis: ( not j in Seg i implies M . j = A . j )

proof

assume A6: j in Seg i ; :: thesis: M . j = B . (F . j)
Seg i c= Seg n by A1, FINSEQ_1:7;
then ( IF . j = F . j & j in Seg n ) by A2, A6, FUNCT_4:14;
then ( Line BIF,j = B . (F . j) & Line BIF,j = BIF . j & (BIF | (Seg i)) . j = BIF . j ) by A3, A6, Th38, FUNCT_1:70, MATRIX_2:10;
hence M . j = B . (F . j) by A3, A6, FUNCT_4:14; :: thesis: verum

end;

assume not j in Seg i ; :: thesis: M . j = A . j
hence M . j = A . j by A3, FUNCT_4:12; :: thesis: verum

end;

A7: for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = m )

proof

let x be set ; :: thesis: ( x in rng M implies ex p being FinSequence of D st
( x = p & len p = m ) )
assume A8: x in rng M ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )
consider k being set such that
A9: ( k in dom M & M . k = x ) by A8, FUNCT_1:def 5;
reconsider k = k as Nat by A9;

per cases ( k in Seg i or not k in Seg i ) ;

suppose A10: k in Seg i ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )

then A11: ( F . k in rng F & rng F c= Seg n ) by A2, FUNCT_1:def 5, RELAT_1:def 19;
then reconsider Fk = F . k as Element of NAT by TARSKI:def 3;
take L = Line B,Fk; :: thesis: ( x = L & len L = m )
( B . (F . k) = L & M . k = B . (F . k) & len L = width B & width B = m ) by A1, A5, A10, A11, MATRIX_1:24, MATRIX_1:def 8, MATRIX_2:10;
hence ( x = L & len L = m ) by A9; :: thesis: verum

end;

suppose A12: not k in Seg i ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )

take L = Line A,k; :: thesis: ( x = L & len L = m )
( M . k = A . k & A . k = L & len L = width A & width A = m ) by A1, A4, A5, A9, A12, MATRIX_1:24, MATRIX_1:def 8, MATRIX_2:10;
hence ( x = L & len L = m ) by A9; :: thesis: verum

end;

end;

end;

then reconsider M = M as Matrix of D by MATRIX_1:9;

A13: now

let p be FinSequence of D; :: thesis: ( p in rng M implies len p = m )
assume p in rng M ; :: thesis: len p = m
then ex q being FinSequence of D st
( p = q & len q = m ) by A7;
hence len p = m ; :: thesis: verum

end;

len M = n by A4, FINSEQ_1:def 3;
then reconsider M = M as Matrix of n,m,D by A13, MATRIX_1:def 3;
take M ; :: thesis: ( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
thus ( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) ) by A5; :: thesis: verum