let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A
for f, g being FinSequence of bool the carrier of A st len f >= len g & len g > 0 & I ||^ (len f) = f . (len f) & f . 1 = I & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = I *' (f /. i) ) & I ||^ (len g) = g . (len g) & g . 1 = I & ( for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = I *' (g /. i) ) holds
f | (dom g) = g
let I be Ideal of A; :: thesis: for f, g being FinSequence of bool the carrier of A st len f >= len g & len g > 0 & I ||^ (len f) = f . (len f) & f . 1 = I & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = I *' (f /. i) ) & I ||^ (len g) = g . (len g) & g . 1 = I & ( for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = I *' (g /. i) ) holds
f | (dom g) = g
let f, g be FinSequence of bool the carrier of A; :: thesis: ( len f >= len g & len g > 0 & I ||^ (len f) = f . (len f) & f . 1 = I & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = I *' (f /. i) ) & I ||^ (len g) = g . (len g) & g . 1 = I & ( for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = I *' (g /. i) ) implies f | (dom g) = g )
assume that
A1: ( len f >= len g & len g > 0 & I ||^ (len f) = f . (len f) & f . 1 = I & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = I *' (f /. i) ) ) and
A2: ( I ||^ (len g) = g . (len g) & g . 1 = I & ( for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = I *' (g /. i) ) ) ; :: thesis: f | (dom g) = g
A3: dom f = Seg (len f) by FINSEQ_1:def 3;
A4: dom g = Seg (len g) by FINSEQ_1:def 3;
set f1 = f | (dom g);
A5: dom (f | (dom g)) = dom (f | (Seg (len g))) by FINSEQ_1:def 3
.= (dom f) /\ (Seg (len g)) by RELAT_1:61
.= (Seg (len f)) /\ (Seg (len g)) by FINSEQ_1:def 3
.= Seg (len g) by A1, FINSEQ_1:5, XBOOLE_1:28 ;
A6: dom (f | (dom g)) = dom g by A5, FINSEQ_1:def 3;
A7: for i being Nat st i in dom (f | (dom g)) & i + 1 in dom (f | (dom g)) holds
(f | (dom g)) . (i + 1) = I *' ((f | (dom g)) /. i)
proof
let i be Nat; :: thesis: ( i in dom (f | (dom g)) & i + 1 in dom (f | (dom g)) implies (f | (dom g)) . (i + 1) = I *' ((f | (dom g)) /. i) )
assume A8: ( i in dom (f | (dom g)) & i + 1 in dom (f | (dom g)) ) ; :: thesis: (f | (dom g)) . (i + 1) = I *' ((f | (dom g)) /. i)
A9: dom (f | (dom g)) c= dom f by A3, A5, A1, FINSEQ_1:5;
A10: (f | (dom g)) /. i = (f | (dom g)) . i by A8, PARTFUN1:def 6
.= f . i by A8, A6, FUNCT_1:49
.= f /. i by A8, A9, PARTFUN1:def 6 ;
(f | (dom g)) . (i + 1) = f . (i + 1) by A8, A6, FUNCT_1:49
.= I *' ((f | (dom g)) /. i) by A10, A1, A8, A9 ;
hence (f | (dom g)) . (i + 1) = I *' ((f | (dom g)) /. i) ; :: thesis: verum
end;
f | (dom g) = g
proof
A11: for k being Nat st k in dom (f | (dom g)) holds
(f | (dom g)) . k = g . k
proof
let k be Nat; :: thesis: ( k in dom (f | (dom g)) implies (f | (dom g)) . k = g . k )
defpred S1[ Nat] means ( $1 in dom (f | (dom g)) implies (f | (dom g)) . $1 = g . $1 );
A12: S1[ 0 ]
proof
assume A13: not S1[ 0 ] ; :: thesis: contradiction
reconsider F = f | (dom g) as FinSequence by A5, FINSEQ_1:def 2;
reconsider x = 0 as object ;
x in dom F by A13;
hence contradiction by FINSEQ_3:24; :: thesis: verum
end;
A15: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; :: thesis: ( S1[a] implies S1[a + 1] )
assume that
A16: S1[a] and
A17: a + 1 in dom (f | (dom g)) ; :: thesis: (f | (dom g)) . (a + 1) = g . (a + 1)
per cases ( a in dom (f | (dom g)) or not a in dom (f | (dom g)) ) ;
suppose A18: a in dom (f | (dom g)) ; :: thesis: (f | (dom g)) . (a + 1) = g . (a + 1)
then A19: (f | (dom g)) /. a = (f | (dom g)) . a by PARTFUN1:def 6
.= g /. a by A6, A16, A18, PARTFUN1:def 6 ;
thus (f | (dom g)) . (a + 1) = I *' ((f | (dom g)) /. a) by A7, A17, A18
.= g . (a + 1) by A2, A6, A17, A18, A19 ; :: thesis: verum
end;
suppose A20: not a in dom (f | (dom g)) ; :: thesis: (f | (dom g)) . (a + 1) = g . (a + 1)
reconsider F = f | (dom g) as FinSequence by A5, FINSEQ_1:def 2;
A21: ( a in dom F or a = 0 ) by A17, TOPREALA:2;
A22: 0 < 0 + (len g) by A1;
( 1 <= 1 & 1 <= len g ) by A22, NAT_1:19;
then 1 in dom g by A4;
hence (f | (dom g)) . (a + 1) = g . (a + 1) by A1, A2, A21, A20, FUNCT_1:49; :: thesis: verum
end;
end;
end;
for a being Nat holds S1[a] from NAT_1:sch 2(A12, A15);
 hence ( k in dom (f | (dom g)) implies (f | (dom g)) . k = g . k ) ; :: thesis: verum
end;
reconsider f1 = f | (dom g) as FinSequence by A5, FINSEQ_1:def 2;
thus f | (dom g) = g by A5, FINSEQ_1:def 3, A11; :: thesis: verum
end;
hence f | (dom g) = g ; :: thesis: verum