let L be Z_Lattice; :: thesis: for f being Function of (DivisibleMod L),INT.Ring

for F, G being FinSequence of (DivisibleMod L)

for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let f be Function of (DivisibleMod L),INT.Ring; :: thesis: for F, G being FinSequence of (DivisibleMod L)

for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let F, G be FinSequence of (DivisibleMod L); :: thesis: for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let v be Vector of (DivisibleMod L); :: thesis: ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

set H = (ScFS (v,f,F)) ^ (ScFS (v,f,G));

set I = F ^ G;

A1: len F = len (ScFS (v,f,F)) by defScFSDM;

A2: len ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) = (len (ScFS (v,f,F))) + (len (ScFS (v,f,G))) by FINSEQ_1:22

.= (len F) + (len (ScFS (v,f,G))) by defScFSDM

.= (len F) + (len G) by defScFSDM

.= len (F ^ G) by FINSEQ_1:22 ;

A3: len G = len (ScFS (v,f,G)) by defScFSDM;

for F, G being FinSequence of (DivisibleMod L)

for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let f be Function of (DivisibleMod L),INT.Ring; :: thesis: for F, G being FinSequence of (DivisibleMod L)

for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let F, G be FinSequence of (DivisibleMod L); :: thesis: for v being Vector of (DivisibleMod L) holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let v be Vector of (DivisibleMod L); :: thesis: ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

set H = (ScFS (v,f,F)) ^ (ScFS (v,f,G));

set I = F ^ G;

A1: len F = len (ScFS (v,f,F)) by defScFSDM;

A2: len ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) = (len (ScFS (v,f,F))) + (len (ScFS (v,f,G))) by FINSEQ_1:22

.= (len F) + (len (ScFS (v,f,G))) by defScFSDM

.= (len F) + (len G) by defScFSDM

.= len (F ^ G) by FINSEQ_1:22 ;

A3: len G = len (ScFS (v,f,G)) by defScFSDM;

now :: thesis: for k being Nat st k in dom ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) holds

((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScProductDM L) . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k)))

hence
ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))
by A2, defScFSDM; :: thesis: verum((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScProductDM L) . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k)))

let k be Nat; :: thesis: ( k in dom ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) implies ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b_{1} = (ScProductDM L) . (v,((f . ((F ^ G) /. b_{1})) * ((F ^ G) /. b_{1}))) )

assume A4: k in dom ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) ; :: thesis: ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b_{1} = (ScProductDM L) . (v,((f . ((F ^ G) /. b_{1})) * ((F ^ G) /. b_{1})))

end;assume A4: k in dom ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) ; :: thesis: ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b

per cases then
( k in dom (ScFS (v,f,F)) or ex n being Nat st

( n in dom (ScFS (v,f,G)) & k = (len (ScFS (v,f,F))) + n ) ) by FINSEQ_1:25;

end;

( n in dom (ScFS (v,f,G)) & k = (len (ScFS (v,f,F))) + n ) ) by FINSEQ_1:25;

suppose A5:
k in dom (ScFS (v,f,F))
; :: thesis: ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b_{1} = (ScProductDM L) . (v,((f . ((F ^ G) /. b_{1})) * ((F ^ G) /. b_{1})))

then A6:
k in dom F
by A1, FINSEQ_3:29;

then A7: k in dom (F ^ G) by FINSEQ_3:22;

A8: F /. k = F . k by A6, PARTFUN1:def 6

.= (F ^ G) . k by A6, FINSEQ_1:def 7

.= (F ^ G) /. k by A7, PARTFUN1:def 6 ;

thus ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScFS (v,f,F)) . k by A5, FINSEQ_1:def 7

.= (ScProductDM L) . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k))) by A5, A8, defScFSDM ; :: thesis: verum

end;then A7: k in dom (F ^ G) by FINSEQ_3:22;

A8: F /. k = F . k by A6, PARTFUN1:def 6

.= (F ^ G) . k by A6, FINSEQ_1:def 7

.= (F ^ G) /. k by A7, PARTFUN1:def 6 ;

thus ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScFS (v,f,F)) . k by A5, FINSEQ_1:def 7

.= (ScProductDM L) . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k))) by A5, A8, defScFSDM ; :: thesis: verum

suppose A9:
ex n being Nat st

( n in dom (ScFS (v,f,G)) & k = (len (ScFS (v,f,F))) + n ) ; :: thesis: ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b_{1} = (ScProductDM L) . (v,((f . ((F ^ G) /. b_{1})) * ((F ^ G) /. b_{1})))

( n in dom (ScFS (v,f,G)) & k = (len (ScFS (v,f,F))) + n ) ; :: thesis: ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b

A10:
k in dom (F ^ G)
by A2, A4, FINSEQ_3:29;

consider n being Nat such that

A11: n in dom (ScFS (v,f,G)) and

A12: k = (len (ScFS (v,f,F))) + n by A9;

A13: n in dom G by A3, A11, FINSEQ_3:29;

then A14: G /. n = G . n by PARTFUN1:def 6

.= (F ^ G) . k by A1, A12, A13, FINSEQ_1:def 7

.= (F ^ G) /. k by A10, PARTFUN1:def 6 ;

thus ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScFS (v,f,G)) . n by A11, A12, FINSEQ_1:def 7

.= (ScProductDM L) . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k))) by A11, A14, defScFSDM ; :: thesis: verum

end;consider n being Nat such that

A11: n in dom (ScFS (v,f,G)) and

A12: k = (len (ScFS (v,f,F))) + n by A9;

A13: n in dom G by A3, A11, FINSEQ_3:29;

then A14: G /. n = G . n by PARTFUN1:def 6

.= (F ^ G) . k by A1, A12, A13, FINSEQ_1:def 7

.= (F ^ G) /. k by A10, PARTFUN1:def 6 ;

thus ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScFS (v,f,G)) . n by A11, A12, FINSEQ_1:def 7

.= (ScProductDM L) . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k))) by A11, A14, defScFSDM ; :: thesis: verum