{} in A * by FINSEQ_1:49;
then {{}} c= A * by ZFMISC_1:31;
then reconsider f = the carrier of s --> {{}} as Function of the carrier of s,(bool (A *)) by FUNCOP_1:45;
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:7;
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:7;
hence {} in f . x by TARSKI:def 1; :: thesis: verum
end;
A3: {} is Element of A * by FINSEQ_1:49;
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 object ; :: 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 A4: t = {} by A1;
A5: t = {} ^ {} by A4;
A6: {} in f . x by A2;
{} in f . y by A2;
hence t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } by A5, A6; :: thesis: verum
end;
let t be object ; :: 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
A7: t = a ^ b and
A8: a in f . x and
A9: b in f . y ;
A10: a = {} by A1, A8;
b = {} by A1, A9;
then a ^ b = {} by A10, FINSEQ_1:34;
hence t in f . (x * y) by A2, A7; :: 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 object ; :: 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 A11: t = {} by A1;
now :: thesis: for b being Element of A * st b in f . y holds
{} ^ b in f . x
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:34;
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, A11; :: thesis: verum
end;
let t be object ; :: 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
A12: t = a and
A13: 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 A13;
then a = {} by A1;
hence t in f . (x /" y) by A2, A12; :: 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 object ; :: 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 A14: t = {} by A1;
now :: thesis: for b being Element of A * st b in f . y holds
b ^ {} in f . x
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:34;
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, A14; :: thesis: verum
end;
let t be object ; :: 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
A15: t = a and
A16: 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 A16;
then a = {} by A1;
hence t in f . (y \ x) by A2, A15; :: thesis: verum
end;