defpred S1[ object ] means ex f, g being Function st
( \$1 = [f,g] & f,g form_morphism_between S1,S2 );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] & S1[x] ) ) from take X ; :: thesis: for x being set holds
( x in X iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) )

thus for x being set holds
( x in X iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) :: thesis: verum
proof
let x be set ; :: thesis: ( x in X iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) )

thus ( x in X implies ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) by A1; :: thesis: ( ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) implies x in X )

given f, g being Function such that A2: x = [f,g] and
A3: f,g form_morphism_between S1,S2 ; :: thesis: x in X
( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by ;
then A4: g in PFuncs ( the carrier' of S1, the carrier' of S2) by PARTFUN1:def 3;
( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by ;
then f in PFuncs ( the carrier of S1, the carrier of S2) by PARTFUN1:def 3;
then x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] by ;
hence x in X by A1, A2, A3; :: thesis: verum
end;