set I = { g where g is Function of Q,Q : ( g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) } ;
{ g where g is Function of Q,Q : ( g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) } c= Funcs (Q,Q)
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { g where g is Function of Q,Q : ( g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) } or f in Funcs (Q,Q) )
assume f in { g where g is Function of Q,Q : ( g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) } ; :: thesis: f in Funcs (Q,Q)
then ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ;
hence f in Funcs (Q,Q) ; :: thesis: verum
end;
then reconsider I = { g where g is Function of Q,Q : ( g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) } as Subset of (Funcs (Q,Q)) ;
take I ; :: thesis: for f being object holds
( f in I iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) )
thus for f being object holds
( f in I iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ; :: thesis: verum