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 );
A1: 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 Def7;
hence (MultPlace (f,x)) . 0 in D ; :: thesis: verum
end;
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; :: thesis: S1[m + 1]
assume A4: (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) ;
then m + 2 in dom x by FINSEQ_1:def 3;
then A5: ( x . (m + 2) in rng x & rng x c= D ) by FUNCT_1:def 3;
A6: ( m + 1 <= m + 2 implies m + 1 <= len x ) by A4, XXREAL_0:2;
[((MultPlace (f,x)) . m),(x . (m + 2))] in [:D,D:] by A6, A3, XREAL_1:8, A5, 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 Def7; :: 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;
A7: S2[ 0 ]
proof
let n be Nat; :: thesis: ( n >= 0 + 1 implies (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0 )
assume A8: n >= 0 + 1 ; :: thesis: (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0
(MultPlace (f,(x | n))) . 0 = (x | n) . 1 by Def7
.= x . 1 by FINSEQ_3:112, A8
.= (MultPlace (f,x)) . 0 by Def7 ;
hence (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0 ; :: thesis: verum
end;
A9: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A10: 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 A11: n >= (m + 1) + 1 ; :: thesis: (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1)
then A12: ( m + 2 >= m + 1 & n >= m + 2 ) by XREAL_1:8;
(MultPlace (f,(x | n))) . (m + 1) = f . (((MultPlace (f,(x | n))) . m),((x | n) . (m + 2))) by Def7
.= f . (((MultPlace (f,x)) . m),((x | n) . (m + 2))) by A10, XXREAL_0:2, A12
.= f . (((MultPlace (f,x)) . m),(x . (m + 2))) by A11, FINSEQ_3:112
.= (MultPlace (f,x)) . (m + 1) by Def7 ;
hence (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1) ; :: thesis: verum
end;
defpred S3[ Nat] means ( S2[$1] & S1[$1] );
A13: S3[ 0 ] by A7, A1;
A14: for m being Nat st S3[m] holds
S3[m + 1] by A9, A2;
for m being Nat holds S3[m] from NAT_1:sch 2(A13, A14);
 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