let R be Ring; :: thesis: for S being Subring of R
for F being non empty FinSequence of the carrier of R
for G being non empty FinSequence of the carrier of S st F = G holds
Product F = Product G
let S be Subring of R; :: thesis: for F being non empty FinSequence of the carrier of R
for G being non empty FinSequence of the carrier of S st F = G holds
Product F = Product G
let F be non empty FinSequence of the carrier of R; :: thesis: for G being non empty FinSequence of the carrier of S st F = G holds
Product F = Product G
let G be non empty FinSequence of the carrier of S; :: thesis: ( F = G implies Product F = Product G )
assume AS: F = G ; :: thesis: Product F = Product G
defpred S₁[ Nat] means for F being non empty FinSequence of the carrier of R
for G being non empty FinSequence of the carrier of S st len F = $1 & F = G holds
Product F = Product G;
A: S₁[ 0 ] ;

B: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for F being non empty FinSequence of the carrier of R
for G being non empty FinSequence of the carrier of S st len F = k + 1 & F = G holds
Product F = Product G

let F be non empty FinSequence of the carrier of R; :: thesis: for G being non empty FinSequence of the carrier of S st len F = k + 1 & F = G holds
Product b₂ = Product b₃
let G be non empty FinSequence of the carrier of S; :: thesis: ( len F = k + 1 & F = G implies Product b₁ = Product b₂ )
assume B1: ( len F = k + 1 & F = G ) ; :: thesis: Product b₁ = Product b₂
consider F1 being FinSequence, x being object such that
B2: F = F1 ^ <*x*> by FINSEQ_1:46;
H: rng F c= the carrier of R by FINSEQ_1:def 4;
rng F1 c= rng F by B2, FINSEQ_1:29;
then reconsider F1 = F1 as FinSequence of the carrier of R by XBOOLE_1:1, H, FINSEQ_1:def 4;
len <*x*> = 1 by FINSEQ_1:40;
then C4: dom F = Seg ((len F1) + 1) by B2, FINSEQ_1:def 7;
B4: len F = (len F1) + (len <*x*>) by B2, FINSEQ_1:22
.= (len F1) + 1 by FINSEQ_1:39 ;
B12: 1 <= (len F1) + 1 by NAT_1:11;
dom <*x*> = Seg 1 by FINSEQ_1:38;
then B11: 1 in dom <*x*> by FINSEQ_1:3;
D20: x = <*x*> . 1
.= F . ((len F1) + 1) by B11, B2, FINSEQ_1:def 7 ;
then B13: x in rng F by B12, C4, FINSEQ_1:1, FUNCT_1:3;
rng F c= the carrier of R by FINSEQ_1:def 4;
then reconsider x = x as Element of the carrier of R by B13;
consider G1 being FinSequence, y being object such that
D2: G = G1 ^ <*y*> by FINSEQ_1:46;
H: rng G c= the carrier of S by FINSEQ_1:def 4;
rng G1 c= rng G by D2, FINSEQ_1:29;
then reconsider G1 = G1 as FinSequence of the carrier of S by XBOOLE_1:1, H, FINSEQ_1:def 4;
len <*y*> = 1 by FINSEQ_1:40;
then C4: dom G = Seg ((len G1) + 1) by D2, FINSEQ_1:def 7;
D4: len G = (len G1) + (len <*y*>) by D2, FINSEQ_1:22
.= (len G1) + 1 by FINSEQ_1:39 ;
B12: 1 <= (len G1) + 1 by NAT_1:11;
dom <*y*> = Seg 1 by FINSEQ_1:38;
then B11: 1 in dom <*y*> by FINSEQ_1:3;
D21: y = <*y*> . 1
.= G . ((len G1) + 1) by B11, D2, FINSEQ_1:def 7 ;
then B13: y in rng G by B12, C4, FINSEQ_1:1, FUNCT_1:3;
rng G c= the carrier of S by FINSEQ_1:def 4;
then reconsider y = y as Element of the carrier of S by B13;
B14: G1 = F1

proof

now :: thesis: for k being Nat st 1 <= k & k <= len G1 holds
G1 . k = F1 . k

let k be Nat; :: thesis: ( 1 <= k & k <= len G1 implies G1 . k = F1 . k )
assume ( 1 <= k & k <= len G1 ) ; :: thesis: G1 . k = F1 . k
then ( k in Seg (len F1) & k in Seg (len G1) ) by B1, B4, D4, FINSEQ_1:1;
then K: ( k in dom F1 & k in dom G1 ) by FINSEQ_1:def 3;
hence G1 . k = F . k by B1, D2, FINSEQ_1:def 7
.= F1 . k by K, B2, FINSEQ_1:def 7 ;
:: thesis: verum

end;

hence G1 = F1 by B1, B4, D4, FINSEQ_1:14; :: thesis: verum

end;

per cases ( not F1 is empty or F1 is empty ) ;

suppose not F1 is empty ; :: thesis: Product b₁ = Product b₂

then E: Product G1 = Product F1 by B0, B1, B4, B14;
thus Product F = (Product F1) * x by B2, GROUP_4:6
.= (Product G1) * y by E, B1, B14, D20, D21, FIELD_6:16
.= Product G by D2, GROUP_4:6 ; :: thesis: verum

end;

suppose F1 is empty ; :: thesis: Product b₁ = Product b₂

then ( F = <*x*> & G = <*y*> ) by B14, B2, D2, FINSEQ_1:34;
then ( Product F = x & Product G = y ) by GROUP_4:9;
hence Product F = Product G by B1, B14, D20, D21; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
consider n being Nat such that
H: n = len F ;
thus Product F = Product G by I, H, AS; :: thesis: verum