let I1, I2 be Subset of (Funcs (Q,Q)); :: thesis: ( ( for f being object holds
( f in I1 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) & ( for f being object holds
( f in I2 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ) implies I1 = I2 )
assume that
A8: for f being object holds
( f in I1 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) and
A9: for f being object holds
( f in I2 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ; :: thesis: I1 = I2
for f being object holds
( f in I1 iff f in I2 )

proof

let f be object ; :: thesis: ( f in I1 iff f in I2 )
( f in I1 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) by A8;
hence ( f in I1 iff f in I2 ) by A9; :: thesis: verum

end;

hence I1 = I2 by TARSKI:2; :: thesis: verum