defpred S₁[ object ] means ( $1 in P * & ex p, q being FinSequence ex n being Nat st
( $1 = p ^ q & p in P & n = A . p & q in U ^^ n ) );
let Y1, Y2 be Subset of (P *); :: thesis: ( ( for a being object holds
( a in Y1 iff ( a in P * & ex p, q being FinSequence ex n being Nat st
( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) ) & ( for a being object holds
( a in Y2 iff ( a in P * & ex p, q being FinSequence ex n being Nat st
( a = p ^ q & p in P & n = A . p & q in U ^^ n ) ) ) ) implies Y1 = Y2 )
assume that
A1: for a being object holds
( a in Y1 iff S₁[a] ) and
A2: for a being object holds
( a in Y2 iff S₁[a] ) ; :: thesis: Y1 = Y2
thus Y1 = Y2 from XBOOLE_0:sch 2(A1, A2); :: thesis: verum