{} in A * by FINSEQ_1:66;
then {{} } c= A * by ZFMISC_1:37;
then reconsider f = the carrier of s --> {{} } as Function of the carrier of s,(bool (A * )) by FUNCOP_1:57;
A1: for x being type of s
for t being set st t in f . x holds
t = {}

proof

let x be type of s; :: thesis: for t being set st t in f . x holds
t = {}
let t be set ; :: thesis: ( t in f . x implies t = {} )
assume t in f . x ; :: thesis: t = {}
then t in {{} } by FUNCOP_1:13;
hence t = {} by TARSKI:def 1; :: thesis: verum

end;

A2: for x being type of s holds {} in f . x

proof

let x be type of s; :: thesis: {} in f . x
f . x = {{} } by FUNCOP_1:13;
hence {} in f . x by TARSKI:def 1; :: thesis: verum

end;

A3: {} is Element of A * by FINSEQ_1:66;
take f ; :: thesis: for x, y being type of s holds
( f . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } & f . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in f . y holds
a1 ^ b in f . x } & f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds
b ^ a2 in f . x } )
let x, y be type of s; :: thesis: ( f . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } & f . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in f . y holds
a1 ^ b in f . x } & f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds
b ^ a2 in f . x } )
thus f . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } :: thesis: ( f . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in f . y holds
a1 ^ b in f . x } & f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds
b ^ a2 in f . x } )

proof

thus f . (x * y) c= { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } :: according to XBOOLE_0:def 10 :: thesis: { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } c= f . (x * y)

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in f . (x * y) or t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } )
assume t in f . (x * y) ; :: thesis: t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) }
then t = {} by A1;
then ( t = {} ^ {} & {} in f . x & {} in f . y ) by A2, FINSEQ_1:47;
hence t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } ; :: thesis: verum

end;

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } or t in f . (x * y) )
assume t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } ; :: thesis: t in f . (x * y)
then consider a, b being Element of A * such that
A4: ( t = a ^ b & a in f . x & b in f . y ) ;
( a = {} & b = {} ) by A1, A4;
then a ^ b = {} by FINSEQ_1:47;
hence t in f . (x * y) by A2, A4; :: thesis: verum

end;

thus f . (x /" y) = { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x } :: thesis: f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds
b ^ a2 in f . x }

proof

thus f . (x /" y) c= { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x } :: according to XBOOLE_0:def 10 :: thesis: { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x } c= f . (x /" y)

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in f . (x /" y) or t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x } )
assume t in f . (x /" y) ; :: thesis: t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x }
then A5: t = {} by A1;

now

let b be Element of A * ; :: thesis: ( b in f . y implies {} ^ b in f . x )
assume b in f . y ; :: thesis: {} ^ b in f . x
then b = {} by A1;
then {} ^ b = {} by FINSEQ_1:47;
hence {} ^ b in f . x by A2; :: thesis: verum

end;

hence t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x } by A3, A5; :: thesis: verum

end;

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x } or t in f . (x /" y) )
assume t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
a ^ b in f . x } ; :: thesis: t in f . (x /" y)
then consider a being Element of A * such that
A6: ( t = a & ( for b being Element of A * st b in f . y holds
a ^ b in f . x ) ) ;
{} in f . y by A2;
then a ^ {} in f . x by A6;
then a in f . x by FINSEQ_1:47;
then a = {} by A1;
hence t in f . (x /" y) by A2, A6; :: thesis: verum

end;

thus f . (y \ x) = { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x } :: thesis: verum

proof

thus f . (y \ x) c= { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x } :: according to XBOOLE_0:def 10 :: thesis: { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x } c= f . (y \ x)

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in f . (y \ x) or t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x } )
assume t in f . (y \ x) ; :: thesis: t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x }
then A7: t = {} by A1;

now

let b be Element of A * ; :: thesis: ( b in f . y implies b ^ {} in f . x )
assume b in f . y ; :: thesis: b ^ {} in f . x
then b = {} by A1;
then b ^ {} = {} by FINSEQ_1:47;
hence b ^ {} in f . x by A2; :: thesis: verum

end;

hence t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x } by A3, A7; :: thesis: verum

end;

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x } or t in f . (y \ x) )
assume t in { a where a is Element of A * : for b being Element of A * st b in f . y holds
b ^ a in f . x } ; :: thesis: t in f . (y \ x)
then consider a being Element of A * such that
A8: ( t = a & ( for b being Element of A * st b in f . y holds
b ^ a in f . x ) ) ;
{} in f . y by A2;
then {} ^ a in f . x by A8;
then a in f . x by FINSEQ_1:47;
then a = {} by A1;
hence t in f . (y \ x) by A2, A8; :: thesis: verum

end;