let L be Z_Lattice; :: thesis: for f being Function of (),INT.Ring
for F, G being FinSequence of ()
for v being Vector of () holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let f be Function of (),INT.Ring; :: thesis: for F, G being FinSequence of ()
for v being Vector of () holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))

let F, G be FinSequence of (); :: thesis: for v being Vector of () holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))
let v be Vector of (); :: 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 = () . (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))) . b1 = () . (v,((f . ((F ^ G) /. b1)) * ((F ^ G) /. b1))) )
assume A4: k in dom ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) ; :: thesis: ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b1 = () . (v,((f . ((F ^ G) /. b1)) * ((F ^ G) /. b1)))
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;
suppose A5: k in dom (ScFS (v,f,F)) ; :: thesis: ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . b1 = () . (v,((f . ((F ^ G) /. b1)) * ((F ^ G) /. b1)))
then A6: k in dom F by ;
then A7: k in dom (F ^ G) by FINSEQ_3:22;
A8: F /. k = F . k by
.= (F ^ G) . k by
.= (F ^ G) /. k by ;
thus ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScFS (v,f,F)) . k by
.= () . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k))) by ; :: thesis: verum
end;
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))) . b1 = () . (v,((f . ((F ^ G) /. b1)) * ((F ^ G) /. b1)))
A10: k in dom (F ^ G) by ;
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 ;
then A14: G /. n = G . n by PARTFUN1:def 6
.= (F ^ G) . k by
.= (F ^ G) /. k by ;
thus ((ScFS (v,f,F)) ^ (ScFS (v,f,G))) . k = (ScFS (v,f,G)) . n by
.= () . (v,((f . ((F ^ G) /. k)) * ((F ^ G) /. k))) by ; :: thesis: verum
end;
end;
end;
hence ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G)) by ; :: thesis: verum