let K1, K2 be Matrix of K; :: thesis: ( len K1 = len b1 & ( for k being Nat st k in dom b1 holds

K1 /. k = (f . (b1 /. k)) |-- b2 ) & len K2 = len b1 & ( for k being Nat st k in dom b1 holds

K2 /. k = (f . (b1 /. k)) |-- b2 ) implies K1 = K2 )

assume that

A10: len K1 = len b1 and

A11: for k being Nat st k in dom b1 holds

K1 /. k = (f . (b1 /. k)) |-- b2 and

A12: len K2 = len b1 and

A13: for k being Nat st k in dom b1 holds

K2 /. k = (f . (b1 /. k)) |-- b2 ; :: thesis: K1 = K2

for k being Nat st 1 <= k & k <= len K1 holds

K1 . k = K2 . k

K1 /. k = (f . (b1 /. k)) |-- b2 ) & len K2 = len b1 & ( for k being Nat st k in dom b1 holds

K2 /. k = (f . (b1 /. k)) |-- b2 ) implies K1 = K2 )

assume that

A10: len K1 = len b1 and

A11: for k being Nat st k in dom b1 holds

K1 /. k = (f . (b1 /. k)) |-- b2 and

A12: len K2 = len b1 and

A13: for k being Nat st k in dom b1 holds

K2 /. k = (f . (b1 /. k)) |-- b2 ; :: thesis: K1 = K2

for k being Nat st 1 <= k & k <= len K1 holds

K1 . k = K2 . k

proof

hence
K1 = K2
by A10, A12, FINSEQ_1:14; :: thesis: verum
let k be Nat; :: thesis: ( 1 <= k & k <= len K1 implies K1 . k = K2 . k )

assume A14: ( 1 <= k & k <= len K1 ) ; :: thesis: K1 . k = K2 . k

then A15: k in dom b1 by A10, FINSEQ_3:25;

A16: k in dom K2 by A10, A12, A14, FINSEQ_3:25;

k in dom K1 by A14, FINSEQ_3:25;

hence K1 . k = K1 /. k by PARTFUN1:def 6

.= (f . (b1 /. k)) |-- b2 by A11, A15

.= K2 /. k by A13, A15

.= K2 . k by A16, PARTFUN1:def 6 ;

:: thesis: verum

end;assume A14: ( 1 <= k & k <= len K1 ) ; :: thesis: K1 . k = K2 . k

then A15: k in dom b1 by A10, FINSEQ_3:25;

A16: k in dom K2 by A10, A12, A14, FINSEQ_3:25;

k in dom K1 by A14, FINSEQ_3:25;

hence K1 . k = K1 /. k by PARTFUN1:def 6

.= (f . (b1 /. k)) |-- b2 by A11, A15

.= K2 /. k by A13, A15

.= K2 . k by A16, PARTFUN1:def 6 ;

:: thesis: verum