let s be SortSymbol of F₁(); :: thesis: for x being Element of F₂() . s holds S₁[x -term ]
let x be Element of F₂() . s; :: thesis: S₁[x -term ]
x -term in F₃() by Th24;
hence S₁[x -term ] by A1; :: thesis: verum

let o be OperSymbol of F₁(); :: thesis: for p being Element of Args (o,(Free (F₁(),F₂()))) st ( for t being Element of (Free (F₁(),F₂())) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]
let p be Element of Args (o,(Free (F₁(),F₂()))); :: thesis: ( ( for t being Element of (Free (F₁(),F₂())) st t in rng p holds
S₁[t] ) implies S₁[o -term p] )
assume A5: for t being Element of (Free (F₁(),F₂())) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]
thus S₁[o -term p] :: thesis: verum