let D be non empty set ; :: thesis: for f being BinOp of D
for x being FinSequence of D
for m being Nat holds
( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds
(MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) )
let f be BinOp of D; :: thesis: for x being FinSequence of D
for m being Nat holds
( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds
(MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) )
let x be FinSequence of D; :: thesis: for m being Nat holds
( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds
(MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) )
defpred S1[ Nat] means ( $1 + 1 <= len x implies (MultPlace (f,x)) . $1 in D );
C0: S1[ 0 ]
proof
assume 0 + 1 <= len x ; :: thesis: (MultPlace (f,x)) . 0 in D
then 1 in Seg (len x) ;
then 1 in dom x by FINSEQ_1:def 3;
then ( x . 1 in rng x & rng x c= D ) by FUNCT_1:def 3;
then ( x . 1 in D & (MultPlace (f,x)) . 0 = x . 1 ) by DefMultPlace;
hence (MultPlace (f,x)) . 0 in D ; :: thesis: verum
end;
C1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume E0: S1[m] ; :: thesis: S1[m + 1]
assume E1: (m + 1) + 1 <= len x ; :: thesis: (MultPlace (f,x)) . (m + 1) in D
then ( m + 2 <= len x & 1 <= m + 2 ) by NAT_1:12;
then m + 2 in Seg (len x) by FINSEQ_1:1;
then m + 2 in dom x by FINSEQ_1:def 3;
then Z1: ( x . (m + 2) in rng x & rng x c= D ) by FUNCT_1:def 3;
Z3: ( m + 1 <= m + 2 implies m + 1 <= len x ) by E1, XXREAL_0:2;
[((MultPlace (f,x)) . m),(x . (m + 2))] in [:D,D:] by Z3, E0, Z1, XREAL_1:6, ZFMISC_1:def 2;
then f . (((MultPlace (f,x)) . m),(x . (m + 2))) in D by FUNCT_2:5;
hence (MultPlace (f,x)) . (m + 1) in D by DefMultPlace; :: thesis: verum
end;
defpred S2[ Nat] means for n being Nat st n >= $1 + 1 holds
(MultPlace (f,(x | n))) . $1 = (MultPlace (f,x)) . $1;
B0: S2[ 0 ]
proof
let n be Nat; :: thesis: ( n >= 0 + 1 implies (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0 )
assume Z1: n >= 0 + 1 ; :: thesis: (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0
(MultPlace (f,(x | n))) . 0 = (x | n) . 1 by DefMultPlace
.= x . 1 by Z1, FINSEQ_3:112
.= (MultPlace (f,x)) . 0 by DefMultPlace ;
hence (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0 ; :: thesis: verum
end;
B1: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume C1: S2[m] ; :: thesis: S2[m + 1]
let n be Nat; :: thesis: ( n >= (m + 1) + 1 implies (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1) )
assume C2: n >= (m + 1) + 1 ; :: thesis: (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1)
then Z2: ( m + 2 >= m + 1 & n >= m + 2 ) by XREAL_1:6;
(MultPlace (f,(x | n))) . (m + 1) = f . (((MultPlace (f,(x | n))) . m),((x | n) . (m + 2))) by DefMultPlace
.= f . (((MultPlace (f,x)) . m),((x | n) . (m + 2))) by C1, Z2, XXREAL_0:2
.= f . (((MultPlace (f,x)) . m),(x . (m + 2))) by C2, FINSEQ_3:112
.= (MultPlace (f,x)) . (m + 1) by DefMultPlace ;
hence (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1) ; :: thesis: verum
end;
defpred S3[ Nat] means ( S2[$1] & S1[$1] );
D0: S3[ 0 ] by B0, C0;
D1: for m being Nat st S3[m] holds
S3[m + 1] by B1, C1;
for m being Nat holds S3[m] from NAT_1:sch 2(D0, D1);
 hence for m being Nat holds
( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds
(MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) ) ; :: thesis: verum