let D be non empty set ; :: thesis: for fD being PFuncs (D,D) -valued FinSequence
for fB being PFuncs (D,BOOLEAN) -valued FinSequence st fD,fB are_composable holds
<*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D
let fD be PFuncs (D,D) -valued FinSequence; :: thesis: for fB being PFuncs (D,BOOLEAN) -valued FinSequence st fD,fB are_composable holds
<*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D
let fB be PFuncs (D,BOOLEAN) -valued FinSequence; :: thesis: ( fD,fB are_composable implies <*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D )
assume that
A1: 1 <= len fD and
A2: len fB = (len fD) + 1 and
A3: for n being Nat st 1 <= n & n <= len fD holds
<*(fB . n),(fD . n),(fB . (n + 1))*> is SFHT of D and
A4: for n being Nat st 2 <= n & n <= len fD holds
<*(PP_inversion (fB . n)),(fD . n),(fB . (n + 1))*> is SFHT of D ; :: according to NOMIN_8:def 7 :: thesis: <*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D
set G = PP_compositionSeq fD;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len fD implies <*(fB . 1),((PP_compositionSeq fD) . $1),(fB . ($1 + 1))*> is SFHT of D );
A5: S₁[ 0 ] ;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A7: S₁[k] and
A8: 1 <= k + 1 and
A9: k + 1 <= len fD ; :: thesis: <*(fB . 1),((PP_compositionSeq fD) . (k + 1)),(fB . ((k + 1) + 1))*> is SFHT of D

per cases ( k = 0 or k > 0 ) ;

suppose A10: k = 0 ; :: thesis: <*(fB . 1),((PP_compositionSeq fD) . (k + 1)),(fB . ((k + 1) + 1))*> is SFHT of D

(PP_compositionSeq fD) . 1 = fD . 1 by A1, Def5;
hence <*(fB . 1),((PP_compositionSeq fD) . (k + 1)),(fB . ((k + 1) + 1))*> is SFHT of D by A1, A3, A10; :: thesis: verum

end;

suppose k > 0 ; :: thesis: <*(fB . 1),((PP_compositionSeq fD) . (k + 1)),(fB . ((k + 1) + 1))*> is SFHT of D

then A11: 0 + 1 <= k by NAT_1:13;
A12: k < len fD by A9, NAT_1:13;
A13: k <= k + 1 by NAT_1:11;
A14: <*(fB . (k + 1)),(fD . (k + 1)),(fB . ((k + 1) + 1))*> is SFHT of D by A3, A8, A9;
<*(PP_inversion (fB . (k + 1))),(fD . (k + 1)),(fB . ((k + 1) + 1))*> is SFHT of D by A4, A9, A11, XREAL_1:6;
then <*(fB . 1),(PP_composition (((PP_compositionSeq fD) . k),(fD . (k + 1)))),(PP_or ((fB . ((k + 1) + 1)),(fB . ((k + 1) + 1))))*> is SFHT of D by A7, A9, A11, A13, A14, XXREAL_0:2, NOMIN_3:24;
hence <*(fB . 1),((PP_compositionSeq fD) . (k + 1)),(fB . ((k + 1) + 1))*> is SFHT of D by A11, A12, Def5; :: thesis: verum

end;

end;

end;

A15: for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
len (PP_compositionSeq fD) = len fD by A1, Def5;
hence <*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D by A1, A2, A15; :: thesis: verum