let R be Ring; :: thesis: for S being Subring of R
for a, b being FinSequence of S
for A, B being FinSequence of R st a = A & b = B holds
mlt (a,b) = mlt (A,B)
let S be Subring of R; :: thesis: for a, b being FinSequence of S
for A, B being FinSequence of R st a = A & b = B holds
mlt (a,b) = mlt (A,B)
let a, b be FinSequence of S; :: thesis: for A, B being FinSequence of R st a = A & b = B holds
mlt (a,b) = mlt (A,B)
let A, B be FinSequence of R; :: thesis: ( a = A & b = B implies mlt (a,b) = mlt (A,B) )
assume A1: a = A ; :: thesis: ( not b = B or mlt (a,b) = mlt (A,B) )
assume A2: b = B ; :: thesis: mlt (a,b) = mlt (A,B)
A3: dom (mlt (a,b)) = dom (mlt (A,B))

proof

mlt (a,b) = the multF of S .: (a,b) by FVSUM_1:def 7;
then A4: len (mlt (a,b)) = min ((len a),(len b)) by FINSEQ_2:71;
mlt (A,B) = the multF of R .: (A,B) by FVSUM_1:def 7;
then A5: len (mlt (A,B)) = min ((len A),(len B)) by FINSEQ_2:71;
thus dom (mlt (a,b)) = Seg (len (mlt (a,b))) by FINSEQ_1:def 3
.= dom (mlt (A,B)) by A1, A2, A4, A5, FINSEQ_1:def 3 ; :: thesis: verum

end;

A6: for i, j, k being Nat st i in Seg (min (j,k)) holds
( i in Seg j & i in Seg k )

proof

let i, j, k be Nat; :: thesis: ( i in Seg (min (j,k)) implies ( i in Seg j & i in Seg k ) )
assume i in Seg (min (j,k)) ; :: thesis: ( i in Seg j & i in Seg k )
then i in (Seg j) /\ (Seg k) by FINSEQ_2:2;
hence ( i in Seg j & i in Seg k ) by XBOOLE_0:def 4; :: thesis: verum

end;

for i being Nat st i in dom (mlt (a,b)) holds
(mlt (a,b)) . i = (mlt (A,B)) . i

proof

let i be Nat; :: thesis: ( i in dom (mlt (a,b)) implies (mlt (a,b)) . i = (mlt (A,B)) . i )
assume A7: i in dom (mlt (a,b)) ; :: thesis: (mlt (a,b)) . i = (mlt (A,B)) . i
A8: mlt (a,b) = the multF of S .: (a,b) by FVSUM_1:def 7;
i in Seg (len (mlt (a,b))) by A7, FINSEQ_1:def 3;
then i in Seg (min ((len a),(len b))) by A8, FINSEQ_2:71;
then ( i in Seg (len a) & i in Seg (len b) ) by A6;
then a1: ( i in dom a & i in dom b ) by FINSEQ_1:def 3;
then reconsider ai = a . i, bi = b . i as Element of S by FUNCT_1:106;
( i in dom A & i in dom B ) by a1, A1, A2;
then reconsider Ai = A . i, Bi = B . i as Element of R by FUNCT_1:106;
thus (mlt (a,b)) . i = ai * bi by A7, FVSUM_1:60
.= Ai * Bi by A1, A2, FIELD_6:16
.= (mlt (A,B)) . i by A3, A7, FVSUM_1:60 ; :: thesis: verum

end;

hence mlt (a,b) = mlt (A,B) by A3, FINSEQ_1:13; :: thesis: verum