defpred S1[ Element of (Free (F1(),F3()))] means ( $1 is context of F4() implies P1[$1] );
A2: for s being SortSymbol of F1()
for x being Element of F3() . s holds S1[x -term ]
proof
let s be SortSymbol of F1(); :: thesis: for x being Element of F3() . s holds S1[x -term ]
let x be Element of F3() . s; :: thesis: S1[x -term ]
assume x -term is context of F4() ; :: thesis: P1[x -term ]
then ( s = F2() & x = F4() ) by Th27;
hence P1[x -term ] by A0; :: thesis: verum
end;
A3: for o being OperSymbol of F1()
for p being Element of Args (o,(Free (F1(),F3()))) st ( for t being Element of (Free (F1(),F3())) st t in rng p holds
S1[t] ) holds
S1[o -term p]
proof
let o be OperSymbol of F1(); :: thesis: for p being Element of Args (o,(Free (F1(),F3()))) st ( for t being Element of (Free (F1(),F3())) st t in rng p holds
S1[t] ) holds
S1[o -term p]
let p be Element of Args (o,(Free (F1(),F3()))); :: thesis: ( ( for t being Element of (Free (F1(),F3())) st t in rng p holds
S1[t] ) implies S1[o -term p] )
assume that
A4: for t being Element of (Free (F1(),F3())) st t in rng p holds
S1[t] and
A5: o -term p is context of F4() ; :: thesis: P1[o -term p]
p is F4() -context_including by A5, Th53;
then F4() -context_in p in rng p by CIn;
then P1[F4() -context_in p] by A4;
hence P1[o -term p] by A1, A5, Th53; :: thesis: verum
end;
S1[F5()] from MSAFREE5:sch 2(A2, A3);
hence P1[F5()] ; :: thesis: verum