let s be Element of F_{1}(); :: thesis: for t being Element of F_{2}() st P_{1}[s,t] holds

P_{2}[F_{3}(s,t)]

let t be Element of F_{2}(); :: thesis: ( P_{1}[s,t] implies P_{2}[F_{3}(s,t)] )

assume P_{1}[s,t]
; :: thesis: P_{2}[F_{3}(s,t)]

then F_{3}(s,t) in { F_{3}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] }
;

hence P_{2}[F_{3}(s,t)]
by A1; :: thesis: verum

P

let t be Element of F

assume P

then F

hence P