let K be commutative Ring; for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds
the multF of K $$ R1 = the multF of K $$ R2
defpred S1[ Nat] means for f, g being FinSequence of K st f,g are_fiberwise_equipotent & len f = $1 holds
the multF of K $$ f = the multF of K $$ g;
let R1, R2 be FinSequence of K; ( R1,R2 are_fiberwise_equipotent implies the multF of K $$ R1 = the multF of K $$ R2 )
assume A1:
R1,R2 are_fiberwise_equipotent
; the multF of K $$ R1 = the multF of K $$ R2
A2:
len R1 = len R1
;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
reconsider n1 =
n as
Nat ;
let f,
g be
FinSequence of
K;
( f,g are_fiberwise_equipotent & len f = n + 1 implies the multF of K $$ f = the multF of K $$ g )
assume that A5:
f,
g are_fiberwise_equipotent
and A6:
len f = n + 1
;
the multF of K $$ f = the multF of K $$ g
A7:
rng f c= the
carrier of
K
by FINSEQ_1:def 4;
0 + 1
<= n + 1
by NAT_1:13;
then A8:
n + 1
in dom f
by A6, FINSEQ_3:25;
then
f . (n + 1) in rng f
by FUNCT_1:def 3;
then reconsider a =
f . (n + 1) as
Element of
K by A7;
rng f = rng g
by A5, CLASSES1:75;
then
a in rng g
by A8, FUNCT_1:def 3;
then consider m being
Nat such that A9:
m in dom g
and A10:
g . m = a
by FINSEQ_2:10;
A11:
g = (g | m) ^ (g /^ m)
by RFINSEQ:8;
set gg =
g /^ m;
set gm =
g | m;
A12:
1
<= m
by A9, FINSEQ_3:25;
then
max (
0,
(m - 1))
= m - 1
by FINSEQ_2:4;
then reconsider m1 =
m - 1 as
Nat by FINSEQ_2:5;
m in Seg m
by A12;
then A13:
(g | m) . m = a
by A9, A10, RFINSEQ:6;
A14:
m = m1 + 1
;
then
m1 <= m
by NAT_1:11;
then A15:
Seg m1 c= Seg m
by FINSEQ_1:5;
m <= len g
by A9, FINSEQ_3:25;
then
len (g | m) = m
by FINSEQ_1:59;
then A16:
g | m = ((g | m) | m1) ^ <*a*>
by A14, A13, RFINSEQ:7;
set fn =
f | n1;
A17:
f = (f | n1) ^ <*a*>
by A6, RFINSEQ:7;
A18:
(g | m) | m1 =
g | ((Seg m) /\ (Seg m1))
by RELAT_1:71
.=
g | m1
by A15, XBOOLE_1:28
;
now for x being object holds card (Coim ((f | n1),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))let x be
object ;
card (Coim ((f | n1),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
card (Coim (f,x)) = card (Coim (g,x))
by A5, CLASSES1:def 10;
then (card ((f | n1) " {x})) + (card (<*a*> " {x})) =
card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})
by A11, A16, A18, A17, FINSEQ_3:57
.=
(card (((g | m1) ^ <*a*>) " {x})) + (card ((g /^ m) " {x}))
by FINSEQ_3:57
.=
((card ((g | m1) " {x})) + (card (<*a*> " {x}))) + (card ((g /^ m) " {x}))
by FINSEQ_3:57
.=
((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*a*> " {x}))
.=
(card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*a*> " {x}))
by FINSEQ_3:57
;
hence
card (Coim ((f | n1),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
;
verum end;
then A19:
f | n1,
(g | m1) ^ (g /^ m) are_fiberwise_equipotent
by CLASSES1:def 10;
len (f | n1) = n
by A6, FINSEQ_1:59, NAT_1:11;
then
the
multF of
K $$ (f | n1) = the
multF of
K $$ ((g | m1) ^ (g /^ m))
by A4, A19;
hence the
multF of
K $$ f =
( the multF of K $$ ((g | m1) ^ (g /^ m))) * ( the multF of K $$ <*a*>)
by A17, FINSOP_1:5
.=
(( the multF of K $$ (g | m1)) * ( the multF of K $$ (g /^ m))) * ( the multF of K $$ <*a*>)
by FINSOP_1:5
.=
(( the multF of K $$ (g | m1)) * ( the multF of K $$ <*a*>)) * ( the multF of K $$ (g /^ m))
by GROUP_1:def 3
.=
( the multF of K $$ (g | m)) * ( the multF of K $$ (g /^ m))
by A16, A18, FINSOP_1:5
.=
the
multF of
K $$ g
by A11, FINSOP_1:5
;
verum
end;
A20:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A20, A3);
hence
the multF of K $$ R1 = the multF of K $$ R2
by A1, A2; verum