let s be Element of F₁(); :: thesis: for t being Element of F₂() st P₁[s,t] holds
P₂[F₃(s,t)]
let t be Element of F₂(); :: thesis: ( P₁[s,t] implies P₂[F₃(s,t)] )
assume P₁[s,t] ; :: thesis: P₂[F₃(s,t)]
then F₃(s,t) in { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₁[s1,t1] } ;
hence P₂[F₃(s,t)] by A1; :: thesis: verum