let D be non empty set ; :: thesis: for f1, f2, f3, f4 being BinominativeFunction of D

for p, q, r, t, w being PartialPredicate of D st <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D & <*(PP_inversion w),f4,t*> is SFHT of D holds

<*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D

let f1, f2, f3, f4 be BinominativeFunction of D; :: thesis: for p, q, r, t, w being PartialPredicate of D st <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D & <*(PP_inversion w),f4,t*> is SFHT of D holds

<*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D

let p, q, r, t, w be PartialPredicate of D; :: thesis: ( <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D & <*(PP_inversion w),f4,t*> is SFHT of D implies <*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D )

assume that

A1: <*p,f1,q*> is SFHT of D and

A2: <*q,f2,r*> is SFHT of D and

A3: <*r,f3,w*> is SFHT of D and

A4: <*w,f4,t*> is SFHT of D and

A5: <*(PP_inversion q),f2,r*> is SFHT of D and

A6: <*(PP_inversion r),f3,w*> is SFHT of D and

A7: <*(PP_inversion w),f4,t*> is SFHT of D ; :: thesis: <*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D

<*p,(PP_composition (f1,f2)),r*> is SFHT of D by A1, A2, A5, NOMIN_3:25;

then <*p,(PP_composition ((PP_composition (f1,f2)),f3)),w*> is SFHT of D by A3, A6, NOMIN_3:25;

hence <*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D by A4, A7, NOMIN_3:25; :: thesis: verum

for p, q, r, t, w being PartialPredicate of D st <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D & <*(PP_inversion w),f4,t*> is SFHT of D holds

<*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D

let f1, f2, f3, f4 be BinominativeFunction of D; :: thesis: for p, q, r, t, w being PartialPredicate of D st <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D & <*(PP_inversion w),f4,t*> is SFHT of D holds

<*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D

let p, q, r, t, w be PartialPredicate of D; :: thesis: ( <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*w,f4,t*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D & <*(PP_inversion w),f4,t*> is SFHT of D implies <*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D )

assume that

A1: <*p,f1,q*> is SFHT of D and

A2: <*q,f2,r*> is SFHT of D and

A3: <*r,f3,w*> is SFHT of D and

A4: <*w,f4,t*> is SFHT of D and

A5: <*(PP_inversion q),f2,r*> is SFHT of D and

A6: <*(PP_inversion r),f3,w*> is SFHT of D and

A7: <*(PP_inversion w),f4,t*> is SFHT of D ; :: thesis: <*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D

<*p,(PP_composition (f1,f2)),r*> is SFHT of D by A1, A2, A5, NOMIN_3:25;

then <*p,(PP_composition ((PP_composition (f1,f2)),f3)),w*> is SFHT of D by A3, A6, NOMIN_3:25;

hence <*p,(PP_composition (f1,f2,f3,f4)),t*> is SFHT of D by A4, A7, NOMIN_3:25; :: thesis: verum